proposition: Lemma for_all_map {A B} P Q (f : A -> B) (Hf : forall x, P x -> Q (f x)) : forall l, for_all P l -> for_all Q (map f l).
proof: Proof. intros l;induction l as [|x l IHl];simpl. - auto. - intros [Hx Hl]. split;auto. Defined.
imports: HoTT.Classes.interfaces.abstract_algebra