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