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