proposition: Lemma Forall2_app_inv_l l1 l2 k : Forall2 P (l1 ++ l2) k ↔ ∃ k1 k2, Forall2 P l1 k1 ∧ Forall2 P l2 k2 ∧ k = k1 ++ k2.
proof: Proof. split; [|intros (?&?&?&?&->); by apply Forall2_app]. revert k. induction l1; inv 1; naive_solver. Qed.
imports: stdpp(options)