Properties of the Core evaluation environment

Registering datatypes in an environment adds only constructors of those datatypes, so it keeps the property that no constructor of the environment's factory produces a Boolean, when no registered datatype is named bool.

Key theorem: Env.addDatatypes_constrsNotBool.

theorem Core.Env.addDatatypes_constrsNotBool {E E' : Env} {blocks : List (Lambda.MutualDatatype Unit)} (hE : E.factory.ConstrsNotBool) (hname : ∀ (b : Lambda.MutualDatatype Unit), b ∈ blocks → ∀ (d : Lambda.LDatatype Unit), d ∈ b → d.name ≠ "bool") (h : E.addDatatypes blocks = Except.ok E') : E'.factory.ConstrsNotBool

Registering datatypes keeps ConstrsNotBool. If E's factory has no Boolean-producing constructor and no datatype in blocks is named bool, the environment E' that Env.addDatatypes returns has a factory with none either.