fact: Axiom thm_LENGTH_ZIP : forall {_35980 _35982 : Type'}, forall l1 : list _35980, forall l2 : list _35982, ((@List.length _35980 l1) = (@List.length _35982 l2)) -> (@List.length (prod _35980 _35982) (@ZIP _35980 _35982 l1 l2)) = (@List.length _35982 l2).
imports: coq theory_hol types terms axioms