proposition: Lemma Forall_app_cons A (P : A -> Prop) l e l' : Forall P (l ++ e :: l') -> Forall P (l ++ l').
proof: Proof. rewrite !Forall_app, Forall_cons; ins; desf. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation