proposition: Lemma Forall_app A (P : A -> Prop) l1 l2 : Forall P (l1 ++ l2) <-> Forall P l1 /\ Forall P l2.
proof: Proof. induction l1; ins; [by intuition; vauto|]. by rewrite !Forall_cons, IHl1, and_assoc. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation