proposition: Lemma Forall3_app_inv_r l k k1' k2' : Forall3 P l k (k1' ++ k2') → ∃ l1 l2 k1 k2, l = l1 ++ l2 ∧ k = k1 ++ k2 ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
proof: Proof. revert l k. induction k1' as [|x k1' IH]; simpl; inv 1. - by repeat eexists; eauto. - by repeat eexists; eauto. - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver. Qed.
imports: stdpp(options)