{A B C : Type} (f : A -> B -> C) (l1 : list A) (l2 : list B) (n : nat) defl defr (H : (n < length l1)%nat) (H' : (n < length l2)%nat) (H'' : (n < length (list_map2 f defl defr l1 l2))%nat) (p : length l1 = length l2) : f (nth' l1 n H) (nth' l2 n H') = nth' (list_map2 f defl defr l1 l2) n H''. Proof. revert l2 n defl defr H H' H'' p; simple_list_induction l1 a l1 IHl1; intros l2 n defl defr H H' H'' p. - destruct l2 as [|b l2]. + destruct (not_lt_zero_r _ H). + inversion p. - destruct l2 as [|b l2]. + inversion p. + destruct n. * reflexivity. * erewrite 3 nth'_cons. apply IHl1. by apply path_nat_succ. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum