NF weak partition development: NominalAlphaCompactEnvFreshSupport002.

Type-explicit successor to the compact TEnvFresh constructors.

NFChoice.Foundation.Var and NFChoice.SemanticCore.Var are distinct names in this import context. Every occurrence below is therefore qualified with the exact variable type used by TBinderEnv and TEnvFresh.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.TEnvFresh.nil (support : Finset SemanticCore.Var) : Nominal.TEnvFresh [] support

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.TEnvFresh.consSame {env : Nominal.TBinderEnv} {support : Finset SemanticCore.Var} (x : SemanticCore.Var) (tail : Nominal.TEnvFresh env support) : Nominal.TEnvFresh ((x, x) :: env) support

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.TEnvFresh.consFresh {env : Nominal.TBinderEnv} {support : Finset SemanticCore.Var} (x y : SemanticCore.Var) (hx : x ∉ support) (hy : y ∉ support) (tail : Nominal.TEnvFresh env support) : Nominal.TEnvFresh ((x, y) :: env) support