proposition: Lemma Forall2_app_inv l1 l2 k1 k2 : length l1 = length k1 → Forall2 P (l1 ++ l2) (k1 ++ k2) → Forall2 P l1 k1 ∧ Forall2 P l2 k2.
proof: Proof. rewrite <-Forall2_same_length. induction 1; inv 1; naive_solver. Qed.
imports: stdpp(options)