Documentation

LeanPool.NFWeakPartition.AlphaSupport.NAR4C057C001Part007Stage1

NF weak partition development: NAR4C057C001Part007.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0246 :

nb057AlphaDummy045 ∈ (SemanticCore.Class.cab nb057AlphaDummy202 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy203 (SemanticCore.Class.cv nb057AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy202) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy202 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy203 (SemanticCore.Class.cv nb057AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy202) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0247 (f : SemanticCore.Var) :

nb057AlphaDummy048 f ∈ (SemanticCore.Class.cab (nb057AlphaDummy204 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy205 f) (SemanticCore.Class.cv (nb057AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy204 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy204 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy205 f) (SemanticCore.Class.cv (nb057AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy204 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0248 :

nb057AlphaDummy203 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0249 (f : SemanticCore.Var) :

nb057AlphaDummy205 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0250 :

nb057AlphaDummy203 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0251 (f : SemanticCore.Var) :

nb057AlphaDummy205 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0252 :

nb057AlphaDummy239 ∈ (SemanticCore.Class.cv nb057AlphaDummy239).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy238).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0253 :

nb057AlphaDummy239 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy242 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy243 (SemanticCore.Class.cv nb057AlphaDummy239) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy242) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy242 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy243 (SemanticCore.Class.cv nb057AlphaDummy238) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy242) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0254 (f : SemanticCore.Var) :

nb057AlphaDummy241 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy241 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy240 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0255 (f : SemanticCore.Var) :

nb057AlphaDummy241 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy244 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy245 f) (SemanticCore.Class.cv (nb057AlphaDummy241 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy244 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy244 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy245 f) (SemanticCore.Class.cv (nb057AlphaDummy240 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy244 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0257 (f : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0258 :

nb057AlphaDummy243 ∈ (SemanticCore.Class.cv nb057AlphaDummy243).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0259 (f : SemanticCore.Var) :

nb057AlphaDummy245 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy245 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0260 :

nb057AlphaDummy250 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy250) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy250) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy250).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0262 :

nb057AlphaDummy250 ∈ (SemanticCore.Class.cv nb057AlphaDummy250).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0263 (f : SemanticCore.Var) :

nb057AlphaDummy252 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy252 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0264 :

nb057AlphaDummy257 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy257) (SemanticCore.Class.cv nb057AlphaDummy258)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy257) (SemanticCore.Class.cv nb057AlphaDummy258)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0265 (f : SemanticCore.Var) :

nb057AlphaDummy260 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy260 f)) (SemanticCore.Class.cv (nb057AlphaDummy261 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy260 f)) (SemanticCore.Class.cv (nb057AlphaDummy261 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0266 :

nb057AlphaDummy257 ∈ (SemanticCore.Class.cv nb057AlphaDummy257).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy258).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0267 (f : SemanticCore.Var) :

nb057AlphaDummy260 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy260 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy261 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0268 :

nb057AlphaDummy258 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy257) (SemanticCore.Class.cv nb057AlphaDummy258)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy257) (SemanticCore.Class.cv nb057AlphaDummy258)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0269 (f : SemanticCore.Var) :

nb057AlphaDummy261 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy260 f)) (SemanticCore.Class.cv (nb057AlphaDummy261 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy260 f)) (SemanticCore.Class.cv (nb057AlphaDummy261 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0270 :

nb057AlphaDummy258 ∈ (SemanticCore.Class.cv nb057AlphaDummy257).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy258).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0271 (f : SemanticCore.Var) :

nb057AlphaDummy261 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy260 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy261 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0272 :

nb057AlphaDummy257 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy257)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy258)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0273 (f : SemanticCore.Var) :

nb057AlphaDummy260 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy260 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy261 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0274 :

nb057AlphaDummy257 ∈ (SemanticCore.Class.cv nb057AlphaDummy257).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy257).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0275 (f : SemanticCore.Var) :

nb057AlphaDummy260 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy260 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy260 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0276 :

nb057AlphaDummy258 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy257)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy258)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0277 (f : SemanticCore.Var) :

nb057AlphaDummy261 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy260 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy261 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0278 :

nb057AlphaDummy258 ∈ (SemanticCore.Class.cv nb057AlphaDummy258).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy258).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0279 (f : SemanticCore.Var) :

nb057AlphaDummy261 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy261 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy261 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0280 :

nb057AlphaDummy238 ∈ (SemanticCore.Class.cv nb057AlphaDummy239).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy238).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0281 :

nb057AlphaDummy238 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy242 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy243 (SemanticCore.Class.cv nb057AlphaDummy239) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy242) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy242 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy243 (SemanticCore.Class.cv nb057AlphaDummy238) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy242) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0282 (f : SemanticCore.Var) :

nb057AlphaDummy240 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy241 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy240 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0283 (f : SemanticCore.Var) :

nb057AlphaDummy240 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy244 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy245 f) (SemanticCore.Class.cv (nb057AlphaDummy241 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy244 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy244 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy245 f) (SemanticCore.Class.cv (nb057AlphaDummy240 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy244 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0284 :

nb057AlphaDummy238 ∈ (SemanticCore.Class.cab nb057AlphaDummy242 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy243 (SemanticCore.Class.cv nb057AlphaDummy238) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy242) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy242 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy243 (SemanticCore.Class.cv nb057AlphaDummy238) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy242) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0285 (f : SemanticCore.Var) :

nb057AlphaDummy240 f ∈ (SemanticCore.Class.cab (nb057AlphaDummy244 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy245 f) (SemanticCore.Class.cv (nb057AlphaDummy240 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy244 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy244 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy245 f) (SemanticCore.Class.cv (nb057AlphaDummy240 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy244 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0286 :

nb057AlphaDummy243 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0287 (f : SemanticCore.Var) :

nb057AlphaDummy245 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0288 :

nb057AlphaDummy243 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0289 (f : SemanticCore.Var) :

nb057AlphaDummy245 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0290 :

nb057AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0291 (f : SemanticCore.Var) :

f ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_compact_fv_empty_0020 :

nb057AlphaDummy000 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_compact_fv_empty_0021 (a : SemanticCore.Var) :

a ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_compact_fv_empty_0022 :

nb057AlphaDummy001 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_compact_fv_empty_0023 (f : SemanticCore.Var) :

f ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_compact_fv_empty_0024 :

nb057AlphaDummy002 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_compact_fv_empty_0025 (f a : SemanticCore.Var) :

nb057AlphaDummy003 f a ∉ ∅