proposition: Lemma baseTypesNotEmpty : BaseType.
proof: Proof. Proof Star. End BT. Module Sig <: Signature. Module BT := BT. Module Export ST := SimpleTypes BT. Inductive FunctionSymbol_aux := a | b | c. Definition FunctionSymbol := FunctionSymbol_aux. Lemma eq_FunctionSymbol_dec : forall f g : FunctionSymbol, {f = g} + {f <> g}. Proof. decide equality. Qed.
imports: CoLoR(TermsSig Horpo HorpoWf RelExtras Terms LogicUtil) Coq(Wf_nat List)