{A B C : Type} (P : A -> Type) (Q : B -> Type) (R : C -> Type) (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)) (l1 : list A) (l2 : list B) : for_all P l1 -> for_all Q l2 -> for_all R (list_map2 f def_l def_r l1 l2). Proof. revert l2; simple_list_induction l1 x l1 IHl1; intro l2. - destruct l2 as [|y l2]; cbn; auto. - simpl. destruct l2 as [|y l2]; intros [Hx Hl1]; [intros _ | intros [Hy Hl2] ]; simpl; auto. apply Hdefl. simpl; auto. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum