proposition: Lemma invIseq2 {A} (x : A) (e : x = x) (iseq : Iseq2 x x eq_refl e) : e = eq_refl.
proof: Proof. generalize_eqs_sig iseq. destruct iseq. simplify ?. simpl. refine (eq_simplification_sigma1_dep _ _ _ _ _). simpl. intros e0. refine (simplify_eq_transport _ _). simpl. revert e0. refine (pack_sigma_eq_inv _ _ _ _ _ _). pose (apply_noConfusion (A := &{ x' : _ & eq w x'})). refine (p _ _ _ _). simpl. unfold NoC_point_l. intros []. trivial. Defined.
imports: Equations(Equations)