proposition: Lemma Forall_append A: forall P n m (v : t A n) (w : t A m), Forall P v -> Forall P w -> Forall P (append v w).
proof: Proof. intros ????? H ?. induction H. - easy. - now constructor. Qed.
imports: VectorDef PeanoNat Eqdep_dec