proposition: Lemma example {A} : &{ Γ' : Tel & 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 (tele (e0 : S n = S n) in (Vector.cons x v ={ vector A ; e0} (Vector.cons y v'))) (fun ρ => inj (ρ.1 = eq_refl))). simpl. refine (equiv_compose _ _). refine (equiv_sym _). refine (equiv_tele_l _). refine (equiv_sym _). refine (injectivity_cons2 &(x, n & v) &(y, n & v')). simpl. pose (lower_solution' A n). pose (inv_equiv e &(x & v)). simpl in e. pose (telei x n in v : telu A). pose (sol:=lifted_solution' (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 (fun x => sigma 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 A n)). specialize (sol (fun x => inj nat)). simpl in e. specialize (sol (fun x => S x.2.1) (fun x => S n) eq_refl eq_refl). simpl in sol. specialize (sol e). subst e. unfold lifted_solution_lhs_type, lifted_solution_lhs_tel_type, lifted_solution_rhs_type in sol. simpl in sol. unfold theorem_square, 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). refine (equiv_tele_r _). intros. unfold square_tel. Lemma subst_dcong_tel {Δ} {Γ : Δ -> Tel} (P : forall x: Δ, Γ x -> Tel) (f : forall x : Δ, Γ x) (s t : Δ) (e : s =={Δ} t) (u : P (f s)) (v : P (f t)) : subst P (dcong_tel f _ _ e) u = unfold cong_tel. simpl. unfold subst. simpl. simpl. rewrite (equiv_cong_subst_tel Transparent telescope eq. unfold telescope. simpl. Opaque eq telescope. simpl. unfold subst. simpl. unfold equiv_sym. unfold injectivity_cons2. simpl. unfold noconf_equiv, equiv, inv_equiv, equiv_inv. simpl. Transparent eq telescope. simpl. unfold noconf_equiv, equiv, inv_equiv, equiv_inv. simpl. clear sol. subst solinst. unfold square_tel. unfold subst. simpl. simpl. refine (equiv_compose _ _). Focus 2. pose (@equiv_cong_subst_tel). specialize (e () Lemma dcong_tel_cong_tel (Δ Γ : Tel) (f : Γ) (u v : Δ) (e : u =={Δ} v) : f =={fun _ => Γ; e} f <~> f == f. Proof. revert v e. refine (J _ _ _). unfold subst. rewrite J_refl. apply equiv_id. Defined.
imports: Equations DepElimDec EqDecInstances Utf8