fact: Fixpoint i2th2 {m : nat} {As : Vector.t A m} (il1 : ilist (B := B) As) (il2 : ilist (B := B') As) (i2l : i2list2 As il1 il2) (n : Fin.t m) : C (ith il1 n) (ith il2 n) := match n in Fin.t m return forall (As : Vector.t A m) (il1 : ilist (B := B) As) (il2 : ilist (B := B') As), i2list2 _ il1 il2 -> C (ith il1 n) (ith il2 n) with | Fin.F1 k => fun As => Vector.caseS (fun n As => forall (il1 : ilist (B := B) As) (il2 : ilist (B := B') As), i2list2 As il1 il2 -> C (ith il1 (@Fin.F1 n)) (ith il2 (@Fin.F1 n))) (fun h n t il1 il2 i2l => i2list2_hd i2l) As | Fin.FS k n' => fun As => Vector_caseS' Fin.t (fun n As n' => forall (il1 : ilist (B := B) As) (il2 : ilist (B := B') As), i2list2 As il1 il2 -> C (ith il1 (@Fin.FS n n')) (ith il2 (@Fin.FS n n'))) (fun h n t m il1 il2 i2l => i2th2 (ilist_tl il1) (ilist_tl il2) (i2list2_tl i2l) m) As n' end As il1 il2 i2l.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common.ilist2