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')). refine (equiv_compose (C:=tele (e : x = y) in (v ={ (λ _ : A, inj (vector A n)); e} v')) _ _). refine (equiv_tele_r _). intros. unfold telescope in x0. simpl in x0. destruct x0. destruct pr2. destruct pr1. simpl in *. unfold injectivity_cons2. simpl. unfold noconf_equiv, equiv, equiv_sym, inv_equiv, equiv_inv. simpl. simpl. intros. eexists. refine (equiv_compose _ _). do 5 intros_tele. 2:simpl. refine (equiv_compose _ _). refine (solution_inv_tele (A:=nat) (Vector.t A) _ _ _). 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')). refine (equiv_compose _ _). refine (equiv_sym _). refine (equiv_tele_l _). refine (equiv' _ _). simpl. unfold equiv', equiv. simpl. refine (equiv_compose _ _). intros_tele. rewrite noConfusion_nat_k3. simpl. unfold telescope. intros_tele. refine (equiv_unit _ _). simpl. refine (equiv_compose _ _). refine (equiv_sym _). refine (equiv_tele_l _). refine (equiv_sym _). refine (noConf_nat_refl_true _). simpl. intros_tele. simpl. refine (equiv_compose _ _). unfold telescope. intros_tele. refine (equiv_id _). refine (equiv_id _). simpl. rewrite noConfusion_nat_k3. simpl. unfold telescope. intros_tele. refine (equiv_unit _ _). 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 (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. 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). refine (equiv_tele_r _). intros. Lemma noConfusion_nat_k2 (x y : nat) (p q : noConf_nat x y) : p = q. Proof. induction x in y, p, q |- *; destruct y. destruct p, q. reflexivity. destruct p. destruct p. simpl in p, q. apply IHx. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances