proposition: Lemma lower_solution : forall A n, forall (x : &{ a : nat & &{ _ : A & &{ _ : vector A a & S a = S n}}}) (P : forall n0 w : nat, A -> vector A w -> S x.1 = S n0 -> Type), (P x.1 x.1 x.2.1 x.2.2.1 eq_refl) -> P n x.1 (x.2).1 ((x.2).2).1 ((x.2).2).2.
proof: Proof. intros A n. curry. intros. revert H. simplify_dep_elim. simplify_dep_elim. simpl. trivial. Defined.
imports: Equations DepElimDec EqDecInstances