length_list_map2@{i j k|} {A : Type@{i}} {B : Type@{j}} {C : Type@{k}} (f : A -> B -> C) defl defr l1 l2 : length l1 = length l2 -> length (list_map2 f defl defr l1 l2) = length l1. Proof. intros p. induction l1 as [|x l1 IHl1] in l2, p |- * using list_ind@{i j}. - destruct l2. + reflexivity. + inversion p. - destruct l2. + inversion p. + cbn; f_ap. by apply IHl1, 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