proposition: Lemma invIseq2d {A} (x : A) (e : x = x) (iseq : Iseq2 x x eq_refl e) : &{ H : eq_refl = e & (H [fun e => Iseq2 x x eq_refl e] # iseq2 x) = iseq }.
proof: Proof. generalize_eqs_sig iseq. destruct iseq. simplify ?. simpl. refine (eq_simplification_sigma1_dep_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 []. intros ->. simpl. intros ->. exists eq_refl. simpl. exact eq_refl. Defined.
imports: Equations(Equations)