fact: Axiom thm_MAP_FST_ZIP : forall {_35918 _35920 : Type'}, forall l1 : list _35918, forall l2 : list _35920, ((@List.length _35918 l1) = (@List.length _35920 l2)) -> (@List.map (prod _35918 _35920) _35918 (@fst _35918 _35920) (@ZIP _35918 _35920 l1 l2)) = l1.
imports: coq theory_hol types terms axioms