proposition: Lemma for_all_map2 {A B C} P Q R `(f : A -> B -> C) (Hf : forall x y, P x -> Q y -> R (f x y)) def_l (Hdefl : forall l1, for_all P l1 -> for_all R (def_l l1)) def_r (Hdefr : forall l2, for_all Q l2 -> for_all R (def_r l2)) : forall l1 l2, for_all P l1 -> for_all Q l2 -> for_all R (map2 f def_l def_r l1 l2).
proof: Proof. intros l1;induction l1 as [|x l1 IHl1]. - simpl. intros [|y l2] _; auto. - simpl. intros [|y l2] [Hx Hl1];[intros _|intros [Hy Hl2]];simpl;auto. apply Hdefl. simpl;auto. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra