proposition: Lemma eq_eq_above_eq_subtype : forall (U:Type) (P:U -> Prop) (z1 z2 : subtype P), forall h : z1.(wit) = z2.(wit), z1.(pf) =⟨ h ⟩ z2.(pf) -> z1 = z2.
proof: Proof. intros U P [w1 p1] [w2 p2]; simpl; intros h <-. dependent inversion h. reflexivity. Qed.
imports: Coq.Logic(EqdepFacts)