fact: Axiom thm_ZIP : forall {_34542 _34543 _34567 _34568 : Type'} (h1' : _34567) (h2' : _34568) (t1 : list _34567) (t2 : list _34568), ((@ZIP _34542 _34543 (@nil _34542) (@nil _34543)) = (@nil (prod _34542 _34543))) /\ ((@ZIP _34567 _34568 (@cons _34567 h1' t1) (@cons _34568 h2' t2)) = (@cons (prod _34567 _34568) (@pair _34567 _34568 h1' h2') (@ZIP _34567 _34568 t1 t2))).
imports: coq theory_hol types terms axioms