proposition: Lemma Forall_rev_ind (Q : list A → Prop) : Q [] → (∀ x l, P x → Forall P l → Q l → Q (l ++ [x])) → ∀ l, Forall P l → Q l.
proof: Proof. intros ?? l. induction l using rev_ind; auto. rewrite Forall_app, Forall_singleton; intros [??]; auto. Qed.
imports: stdpp(options)