proposition: Lemma all_Forall {X : Type} {P : X -> Prop} {l : list X} : all (map P l) <-> Forall P l.
proof: Proof. elim: l; [done|]. move=> x l IH /=. split. - move=> [? /IH ?]. by constructor. - by move=> /Forall_cons_iff [? /IH ?]. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun