fact: Axiom thm_ITLIST2_DEF : forall {_34449 _34451 _34459 : Type'} (h1' : _34451) (f : _34451 -> _34459 -> _34449 -> _34449) (t1 : list _34451) (l2 : list _34459) (b : _34449), ((@ITLIST2 _34449 _34451 _34459 f (@nil _34451) l2 b) = b) /\ ((@ITLIST2 _34449 _34451 _34459 f (@cons _34451 h1' t1) l2 b) = (f h1' (@hd _34459 l2) (@ITLIST2 _34449 _34451 _34459 f t1 (@tl _34459 l2) b))).
imports: coq theory_hol types terms axioms