{A B} (z z' : W A B) : (w_label z;w_arg z) = (w_label z';w_arg z') :> {a : _ & B a -> W A B} <~> z = z' := (equiv_ap' (issig_W A B)^-1%equiv z z')^-1%equiv.
Require Import HoTT.Basics. Require Import Types.Forall Types.Sigma.