fact: Axiom thm_LAST_APPEND : forall {_36905 : Type'}, forall p : list _36905, forall q : list _36905, (@LAST _36905 (@List.app _36905 p q)) = (@COND _36905 (q = (@nil _36905)) (@LAST _36905 p) (@LAST _36905 q)).
imports: coq theory_hol types terms axioms