proposition: Lemma example@{i j +} {A : Type@{i}} : sigma@{j} (Tel@{i}) (fun Γ' : Tel@{i} => Equiv@{i} (tele (n : nat) (x y : A) (v v' : Vector.t A n) in (Vector.cons x v = Vector.cons y v')) Γ').
proof: Proof. intros. eexists. refine (equiv_compose _ _). do 5 intros_tele. 2:simpl. refine (equiv_compose _ _). refine (solution_inv_tele (A:=nat) (Vector.t A) _ _ _). refine (equiv_compose _ _). refine (reorder_tele@{i j} (ext@{i} _ (fun e0 : S n = S n => inj@{i} (Vector.cons x v ={ vector A ; e0} (Vector.cons y v')))) (fun ρ => inj@{i} (ρ.1 = eq_refl))). simpl. refine (equiv_compose _ _). refine (equiv_sym _). refine (equiv_tele_l _). refine (equiv_sym _). refine (injectivity_cons2@{i i} &(x, n & v) &(y, n & v')). cbn. pose (lower_solution@{i i} A n). pose (inv_equiv e &(x & v)). simpl in e. pose (sol:=lifted_solution@{i j} (tele (_ : A) (n' : nat) in vector A n')). simpl in sol. simpl in t0. unfold e, lower_solution, equiv, equiv_inv, inv_equiv in t0. simpl in t0. unfold e, lower_solution, equiv, equiv_inv, inv_equiv in t0. simpl in t0. set (solinst := sigmaI@{i} (fun x => sigma@{i} nat (fun n => vector A n)) t0.1 &(t0.2.1 & t0.2.2.1)). specialize (sol solinst). specialize (sol &(y, n & v')). specialize (sol (telv@{i i} A n)). specialize (sol (inj@{i} nat)). simpl in sol. specialize (sol (fun x => S x.2.1) (fun x => S n) eq_refl eq_refl). simpl in sol. specialize (sol e). subst e. simpl in sol. unfold solution_left in *. simpl in *. unfold inv_equiv in sol. unfold eq_points_equiv in sol. simpl in *. unfold equiv_inv in *. simpl in *. unfold cong in sol. simpl in *. refine (equiv_compose (C:=tele (e : x = y) in (v ={ (λ _ : A, inj (vector A n)); e} v')) _ sol). simpl. refine (equiv_tele_r _). intros. unfold equiv_sym. unfold injectivity_cons2. simpl. unfold noconf_equiv, equiv, inv_equiv, equiv_inv. simpl. unfold square_tel. simpl. Transparent eq telescope. simpl. clear sol. subst solinst. unfold subst. simpl. rewrite (cong_tel_proj@{i} _ _ (fun x : nat => inj (vector A x)) (λ x0 : tele (_ : A) (n0 : nat) in vector A n0, &(S (x0.2).1 & Vector.cons x0.1 (x0.2).2)) _ _ x0). simpl. Transparent telescope. unfold telescope at 1. simpl telescope. rewrite (cong_tel_nondep@{i} (Γ:=inj nat) (S n) _ _ x0). refine (equiv_id _). simpl. refine (equiv_id _). Defined.
imports: Equations Utf8 DepElimDec EqDecInstances