proposition: Lemma lem_perm_forall {A} (P : A -> Prop) : forall l1 l2, Permutation l1 l2 -> List.Forall P l1 -> List.Forall P l2.
proof: Proof. induction 1; sauto. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation