proposition: Lemma Forall_cons A (P : A -> Prop) a l : Forall P (a :: l) <-> P a /\ Forall P l.
proof: Proof. split; intro H; desf; vauto; inversion H; desf. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation