proposition: Lemma Forall_in A (P : A -> Prop) l x : Forall P l -> In x l -> P x.
proof: Proof. ins; eapply Forall_forall; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation