fact: Axiom thm_EL : forall {_34373 : Type'} (n : nat) (l : list _34373), ((@EL _34373 (NUMERAL 0) l) = (@hd _34373 l)) /\ ((@EL _34373 (S n) l) = (@EL _34373 n (@tl _34373 l))).
imports: coq theory_hol types terms axioms