fact: Axiom thm_LAST_EL : forall {_37078 : Type'}, forall l : list _37078, (~ (l = (@nil _37078))) -> (@LAST _37078 l) = (@EL _37078 (Nat.sub (@List.length _37078 l) (NUMERAL (BIT1 0))) l).
imports: coq theory_hol types terms axioms