proposition: Lemma ITLIST2_def {_34449 _34451 _34459 : Type'} : (@ITLIST2 _34449 _34451 _34459) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (_34451 -> _34459 -> _34449 -> _34449) -> (list _34451) -> (list _34459) -> _34449 -> _34449) (fun ITLIST2' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) -> (_34451 -> _34459 -> _34449 -> _34449) -> (list _34451) -> (list _34459) -> _34449 -> _34449 => forall _18201 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))), (forall f : _34451 -> _34459 -> _34449 -> _34449, forall l2 : list _34459, forall b : _34449, (ITLIST2' _18201 f (@nil _34451) l2 b) = b) /\ (forall h1' : _34451, forall f : _34451 -> _34459 -> _34449 -> _34449, forall t1 : list _34451, forall l2 : list _34459, forall b : _34449, (ITLIST2' _18201 f (@cons _34451 h1' t1) l2 b) = (f h1' (@hd _34459 l2) (ITLIST2' _18201 f t1 (@tl _34459 l2) b)))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0)))))))))))))).
proof: Proof. exact (eq_refl (@ITLIST2 _34449 _34451 _34459)). Qed.
imports: coq theory_hol types