fact: Axiom thm_APPEND_EQ_NIL : forall {_36457 : Type'}, forall l : list _36457, forall m : list _36457, ((@List.app _36457 l m) = (@nil _36457)) = ((l = (@nil _36457)) /\ (m = (@nil _36457))).
imports: coq theory_hol types terms axioms