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