fact: Axiom thm_EL_MAP : forall {_37170 _37171 : Type'}, forall f : _37171 -> _37170, forall n : nat, forall l : list _37171, (Peano.lt n (@List.length _37171 l)) -> (@EL _37170 n (@List.map _37171 _37170 f l)) = (f (@EL _37171 n l)).
imports: coq theory_hol types terms axioms