proposition: Lemma Exists_app l1 l2 : Exists P (l1 ++ l2) ↔ Exists P l1 ∨ Exists P l2.
proof: Proof. split. - induction l1; inv 1; naive_solver. - intros [H|H]; [induction H | induction l1]; simpl; intuition. Qed.
imports: stdpp(options)