proposition: Lemma all_map_impl {X : Type} {P Q : X -> Prop} {l : list X} : (forall x, P x -> Q x) -> all (map P l) -> all (map Q l).
proof: Proof. move=> /Forall_impl H /all_Forall /H ?. by apply /all_Forall. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun