proposition: Lemma Forall2_app_r l k1 k2 : Forall2 P (take (length k1) l) k1 → Forall2 P (drop (length k1) l) k2 → Forall2 P l (k1 ++ k2).
proof: Proof. intros. rewrite <-(take_drop (length k1) l). by apply Forall2_app. Qed.
imports: stdpp(options)