fact: Axiom thm_BUTLAST : forall {_34055 : Type'} (h : _34055) (t : list _34055), ((@List.removelast _34055 (@nil _34055)) = (@nil _34055)) /\ ((@List.removelast _34055 (@cons _34055 h t)) = (@COND (list _34055) (t = (@nil _34055)) (@nil _34055) (@cons _34055 h (@List.removelast _34055 t)))).
imports: coq theory_hol types terms axioms