fact: Axiom thm_LENGTH_EQ_CONS : forall {_35025 : Type'}, forall l : list _35025, forall n : nat, ((@List.length _35025 l) = (S n)) = (exists h : _35025, exists t : list _35025, (l = (@cons _35025 h t)) /\ ((@List.length _35025 t) = n)).
imports: coq theory_hol types terms axioms