proposition: Lemma app_equiv_eq l k1 k2 : l ≡ k1 ++ k2 ↔ ∃ k1' k2', l = k1' ++ k2' ∧ k1' ≡ k1 ∧ k2' ≡ k2.
proof: Proof. split; [|intros (?&?&->&?&?); by f_equiv]. setoid_rewrite list_equiv_Forall2. rewrite Forall2_app_inv_r. naive_solver. Qed.
imports: stdpp(options)