for_all_list_map2' {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 def_r} {l1 : list A} {l2 : list B} (p : length l1 = length l2) : for_all P l1 -> for_all Q l2 -> for_all R (list_map2 f def_l def_r l1 l2). Proof. revert l2 p; simple_list_induction l1 x l1 IHl1; intros l2 p. - destruct l2. + reflexivity. + discriminate. - destruct l2 as [|y l2]. + discriminate. + intros [Hx Hl1] [Hy Hl2]. split. * by apply Hf. * apply IHl1; trivial. apply path_nat_succ. exact p. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum