proposition: Theorem eq_irrelevance (T : eqType) x y : forall e1 e2 : x = y :> T, e1 = e2.
proof: Proof. pose proj z e := if x =P z is ReflectT e0 then e0 else e. suff: injective (proj y) by rewrite /proj => injp e e'; apply: injp; case: eqP. pose join (e : x = _) := etrans (esym e). apply: can_inj (join x y (proj x (erefl x))) _. by case: y /; case: _ / (proj x _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool)