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