proposition: Lemma invIseq2' {A} (x : A) (e : x = x) (iseq : Iseq2 x x e eq_refl) : &{ H : eq_refl = e & (Top.subst (P:=fun e => Iseq2 x x e eq_refl) H (iseq2 x)) = iseq }.
proof: Proof. generalize_eqs_sig iseq. destruct iseq. intros H; symmetry in H. revert H. refine (eq_simplification_sigma1_dep_dep _ _ _ _ _). intros. subst iseq0. revert e'. intros e'. set (eos := the_end_of_the_section). move eos before A. uncurry_hyps pack. pattern sigma pack. clearbody pack. clear. set(vartel := tele (x : A) (e : x = x) (w : A) (e : (&(w, w, eq_refl & eq_refl) = &(x, x, e & eq_refl) :> (tele (x : A) (y : A) (e : x = y) in (y = x)))) in unit). change (telescope vartel) in pack. unfold vartel in pack. clear vartel. revert pack. unshelve refine (apply_equiv_dom _ _ _). shelve. refine (equiv_sym _). - refine (equiv_compose _ _). set(vartel := tele (x : A) (e : x = x) in A). set(eqtel' := (fun x : vartel => tele (_ : &(x.2.2, x.2.2, eq_refl & eq_refl) = &(x.1, x.1, x.2.1 & eq_refl) :> tele (x : A) (y : A) (e : x = y) in (y = x)) in unit)). pose (reorder_tele vartel eqtel'). simpl in e. unfold eqtel' in e. simpl in e. refine e. refine (equiv_compose _ _). refine (equiv_compose _ _). refine (equiv_tele_r _). intros x. set(eqtel := (tele (x : A) (y : A) (e : x = y) in (y = x))). set(vartel := tele (x : A) (e : x = x) in A). set(eqtel'' := (fun x : vartel => tele (_ : &(x.2.2, x.2.2, eq_refl & eq_refl) =={eqtel} &(x.1, x.1, x.2.1 & eq_refl)) in unit)). refine (equiv_compose _ _). refine (equiv_tele_l (B := fun _ => unit) _). apply (@eq_points_equiv eqtel). refine (equiv_id _). cbn. simpl. refine (equiv_id _). refine (equiv_id _). simpl. refine (con simpl. simplify ?. simpl. Lemma noconf : forall (A : Type) (a b : &{ index : nat & vector A index}), a =={ext nat (fun n => inj (vector A n))} b -> NoConf A a b. Proof. intros. destruct X. destruct a, b. simpl in pr1, pr2. destruct pr1. simpl in pr2. destruct pr2. simpl. destruct pr3. simpl. simpl. exact tt. simpl. exists eq_refl. exists eq_refl. simpl. constructor. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances