proposition: Lemma eq_eq_above_eq_nsigT : forall (U:Type) (P:U -> Type) (z1 z2 : { u : U ⫳ P u }), forall h : dfst z1 = dfst z2, dsnd z1 =⟨ h ⟩ dsnd z2 -> z1 = z2.
proof: Proof. intros U P [w1 p1] [w2 p2]; simpl; intros h <-. dependent inversion h. reflexivity. Qed.
imports: Coq.Logic(EqdepFacts)