proposition: Lemma Forall_and {Q} l : Forall (λ x, P x ∧ Q x) l ↔ Forall P l ∧ Forall Q l.
proof: Proof. split; [induction 1; constructor; naive_solver|]. intros [Hl Hl']; revert Hl'; induction Hl; inv 1; auto. Qed.
imports: stdpp(options)