proposition: Lemma Forall_reverse l : Forall P (reverse l) ↔ Forall P l.
proof: Proof. induction l as [|x l IH]; simpl; [done|]. rewrite reverse_cons, Forall_cons, Forall_app, Forall_singleton. naive_solver. Qed.
imports: stdpp(options)