proposition: Lemma Forall2_app_l l1 l2 k : Forall2 P l1 (take (length l1) k) → Forall2 P l2 (drop (length l1) k) → Forall2 P (l1 ++ l2) k.
proof: Proof. intros. rewrite <-(take_drop (length l1) k). by apply Forall2_app. Qed.
imports: stdpp(options)