fact: Axiom thm_MAP_SND_ZIP : forall {_35949 _35951 : Type'}, forall l1 : list _35949, forall l2 : list _35951, ((@List.length _35949 l1) = (@List.length _35951 l2)) -> (@List.map (prod _35949 _35951) _35951 (@snd _35949 _35951) (@ZIP _35949 _35951 l1 l2)) = l2.
imports: coq theory_hol types terms axioms