fact: Axiom thm_ZIP_DEF : forall {_34523 _34531 : Type'} (h1' : _34523) (t1 : list _34523) (l2 : list _34531), ((@ZIP _34523 _34531 (@nil _34523) l2) = (@nil (prod _34523 _34531))) /\ ((@ZIP _34523 _34531 (@cons _34523 h1' t1) l2) = (@cons (prod _34523 _34531) (@pair _34523 _34531 h1' (@hd _34531 l2)) (@ZIP _34523 _34531 t1 (@tl _34531 l2)))).
imports: coq theory_hol types terms axioms