proposition: Lemma lower_solution@{i +} : forall (A : Type@{i}) n, Equiv@{i} (tele (x' : A) (n' : nat) (v : vector A n') in (S n' = S n)) (tele (x : A) in vector A n).
proof: Proof. intros A n. unshelve refine {| equiv a := _ |}. refine &(a.1 & _). destruct a. destruct pr2. destruct pr2. simpl in pr3. noconf pr3. exact pr2. unshelve eapply BuildIsEquiv@{i}. intros a. refine &(a.1, n & _). refine &(a.2 & eq_refl). intro. simpl. unfold solution_left. simpl. reflexivity. intro. simpl. unfold solution_left. unfold NoConfusion.noConfusion_nat_obligation_1. simpl. destruct x. destruct pr2. destruct pr2. simpl. refine (Top.cong@{i i} _ _). revert pr3. simplify_one_dep_elim. simplify_one_dep_elim. intros. reflexivity. intros. simpl. destruct x as (x&n'&v&e). unfold solution_left_dep, apply_noConfusion. simpl. unfold Top.cong. revert e. simpl. simplify_one_dep_elim. simplify_one_dep_elim. intros. reflexivity. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances