fact: Definition language_decidable := ((forall x y : Functions L, {x = y} + {x <> y}) * (forall x y : Relations L, {x = y} + {x <> y}))%type.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )