fact: Axiom thm_LENGTH_MAP2 : forall {_36544 _36546 _36557 : Type'}, forall f : _36544 -> _36546 -> _36557, forall l : list _36544, forall m : list _36546, ((@List.length _36544 l) = (@List.length _36546 m)) -> (@List.length _36557 (@MAP2 _36557 _36544 _36546 f l m)) = (@List.length _36546 m).
imports: coq theory_hol types terms axioms