inlist_map2@{i j k u | i <= u, j <= u, k <= u} {A : Type@{i}} {B : Type@{j}} {C : Type@{k}} (f : A -> B -> C) defl defr l1 l2 x : InList x (list_map2 f defl defr l1 l2) -> length l1 = length l2 -> { y : A & { z : B & prod@{k u} ((f y z) = x) (InList y l1 * InList z l2) } }. Proof. intros H p. induction l1 as [|y l1 IHl1] in l2, x, H, p |- * using list_ind@{i u}. - destruct l2. 1: contradiction. inversion p. - destruct l2 as [| z]. 1: inversion p. destruct H as [q | i]. 1: exact (y; z; (q, (inl idpath, inl idpath))). destruct (IHl1 l2 x i) as [y' [z' [q [r s]]]]. 1: apply path_nat_succ, p. exact (y'; z'; (q, (inr r, inr s))). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum