Nominal proof certificates grouped in dependency order.

Certificates from NAR4C090C001Part017.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0217 (h : SemanticCore.Var) : nb090AlphaDummy054 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy209 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy210 h) (SemanticCore.Class.cv (nb090AlphaDummy054 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy209 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy209 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy210 h) (SemanticCore.Class.cv (nb090AlphaDummy053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy209 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0218 (A : SemanticCore.Class) : nb090AlphaDummy051 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy207 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy208 A) (SemanticCore.Class.cv (nb090AlphaDummy051 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy207 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy207 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy208 A) (SemanticCore.Class.cv (nb090AlphaDummy051 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy207 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0219 (h : SemanticCore.Var) : nb090AlphaDummy054 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy209 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy210 h) (SemanticCore.Class.cv (nb090AlphaDummy054 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy209 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy209 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy210 h) (SemanticCore.Class.cv (nb090AlphaDummy054 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy209 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0220 (A : SemanticCore.Class) : nb090AlphaDummy208 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy208 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0221 (h : SemanticCore.Var) : nb090AlphaDummy210 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy210 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0222 (A : SemanticCore.Class) : nb090AlphaDummy215 A ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy215 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy215 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy215 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0223 (h : SemanticCore.Var) : nb090AlphaDummy217 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy217 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy217 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy217 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0224 (A : SemanticCore.Class) : nb090AlphaDummy215 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy215 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0225 (h : SemanticCore.Var) : nb090AlphaDummy217 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy217 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0226 (A : SemanticCore.Class) : nb090AlphaDummy222 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy222 A)) (SemanticCore.Class.cv (nb090AlphaDummy223 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy222 A)) (SemanticCore.Class.cv (nb090AlphaDummy223 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0227 (h : SemanticCore.Var) : nb090AlphaDummy225 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy225 h)) (SemanticCore.Class.cv (nb090AlphaDummy226 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy225 h)) (SemanticCore.Class.cv (nb090AlphaDummy226 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0228 (A : SemanticCore.Class) : nb090AlphaDummy222 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy222 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy223 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0229 (h : SemanticCore.Var) : nb090AlphaDummy225 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy225 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy226 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0230 (A : SemanticCore.Class) : nb090AlphaDummy223 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy222 A)) (SemanticCore.Class.cv (nb090AlphaDummy223 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy222 A)) (SemanticCore.Class.cv (nb090AlphaDummy223 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0231 (h : SemanticCore.Var) : nb090AlphaDummy226 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy225 h)) (SemanticCore.Class.cv (nb090AlphaDummy226 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy225 h)) (SemanticCore.Class.cv (nb090AlphaDummy226 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0232 (A : SemanticCore.Class) : nb090AlphaDummy223 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy222 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy223 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0233 (h : SemanticCore.Var) : nb090AlphaDummy226 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy225 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy226 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0234 (A : SemanticCore.Class) : nb090AlphaDummy222 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy222 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy223 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0235 (h : SemanticCore.Var) : nb090AlphaDummy225 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy225 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy226 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0236 (A : SemanticCore.Class) : nb090AlphaDummy222 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy222 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy222 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0237 (h : SemanticCore.Var) : nb090AlphaDummy225 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy225 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy225 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0238 (A : SemanticCore.Class) : nb090AlphaDummy223 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy222 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy223 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0239 (h : SemanticCore.Var) : nb090AlphaDummy226 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy225 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy226 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0240 (A : SemanticCore.Class) : nb090AlphaDummy223 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy223 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy223 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0241 (h : SemanticCore.Var) : nb090AlphaDummy226 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy226 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy226 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0242 (A : SemanticCore.Class) : nb090AlphaDummy050 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy051 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy050 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0243 (A : SemanticCore.Class) : nb090AlphaDummy050 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy207 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy208 A) (SemanticCore.Class.cv (nb090AlphaDummy051 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy207 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy207 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy208 A) (SemanticCore.Class.cv (nb090AlphaDummy050 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy207 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0244 (h : SemanticCore.Var) : nb090AlphaDummy053 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy054 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy053 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0245 (h : SemanticCore.Var) : nb090AlphaDummy053 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy209 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy210 h) (SemanticCore.Class.cv (nb090AlphaDummy054 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy209 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy209 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy210 h) (SemanticCore.Class.cv (nb090AlphaDummy053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy209 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0246 (A : SemanticCore.Class) : nb090AlphaDummy050 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy207 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy208 A) (SemanticCore.Class.cv (nb090AlphaDummy050 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy207 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy207 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy208 A) (SemanticCore.Class.cv (nb090AlphaDummy050 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy207 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0247 (h : SemanticCore.Var) : nb090AlphaDummy053 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy209 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy210 h) (SemanticCore.Class.cv (nb090AlphaDummy053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy209 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy209 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy210 h) (SemanticCore.Class.cv (nb090AlphaDummy053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy209 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0248 (A : SemanticCore.Class) : nb090AlphaDummy208 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0249 (h : SemanticCore.Var) : nb090AlphaDummy210 h ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0250 (A : SemanticCore.Class) : nb090AlphaDummy208 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0251 (h : SemanticCore.Var) : nb090AlphaDummy210 h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0252 (A : SemanticCore.Class) : nb090AlphaDummy244 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy244 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy243 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0253 (A : SemanticCore.Class) : nb090AlphaDummy244 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy247 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy248 A) (SemanticCore.Class.cv (nb090AlphaDummy244 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy247 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy247 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy248 A) (SemanticCore.Class.cv (nb090AlphaDummy243 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy247 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0254 (h : SemanticCore.Var) : nb090AlphaDummy246 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy246 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy245 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0255 (h : SemanticCore.Var) : nb090AlphaDummy246 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy249 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy250 h) (SemanticCore.Class.cv (nb090AlphaDummy246 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy249 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy249 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy250 h) (SemanticCore.Class.cv (nb090AlphaDummy245 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy249 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0256 (A : SemanticCore.Class) : nb090AlphaDummy244 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy247 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy248 A) (SemanticCore.Class.cv (nb090AlphaDummy244 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy247 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy247 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy248 A) (SemanticCore.Class.cv (nb090AlphaDummy244 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy247 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0257 (h : SemanticCore.Var) : nb090AlphaDummy246 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy249 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy250 h) (SemanticCore.Class.cv (nb090AlphaDummy246 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy249 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy249 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy250 h) (SemanticCore.Class.cv (nb090AlphaDummy246 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy249 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0258 (A : SemanticCore.Class) : nb090AlphaDummy248 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy248 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0259 (h : SemanticCore.Var) : nb090AlphaDummy250 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy250 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0260 (A : SemanticCore.Class) : nb090AlphaDummy255 A ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy255 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy255 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy255 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0261 (h : SemanticCore.Var) : nb090AlphaDummy257 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy257 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy257 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy257 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0262 (A : SemanticCore.Class) : nb090AlphaDummy255 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy255 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0263 (h : SemanticCore.Var) : nb090AlphaDummy257 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy257 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0264 (A : SemanticCore.Class) : nb090AlphaDummy262 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy262 A)) (SemanticCore.Class.cv (nb090AlphaDummy263 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy262 A)) (SemanticCore.Class.cv (nb090AlphaDummy263 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0265 (h : SemanticCore.Var) : nb090AlphaDummy265 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy265 h)) (SemanticCore.Class.cv (nb090AlphaDummy266 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy265 h)) (SemanticCore.Class.cv (nb090AlphaDummy266 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0266 (A : SemanticCore.Class) : nb090AlphaDummy262 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy262 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy263 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0267 (h : SemanticCore.Var) : nb090AlphaDummy265 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy265 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy266 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0268 (A : SemanticCore.Class) : nb090AlphaDummy263 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy262 A)) (SemanticCore.Class.cv (nb090AlphaDummy263 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy262 A)) (SemanticCore.Class.cv (nb090AlphaDummy263 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0269 (h : SemanticCore.Var) : nb090AlphaDummy266 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy265 h)) (SemanticCore.Class.cv (nb090AlphaDummy266 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy265 h)) (SemanticCore.Class.cv (nb090AlphaDummy266 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0270 (A : SemanticCore.Class) : nb090AlphaDummy263 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy262 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy263 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0271 (h : SemanticCore.Var) : nb090AlphaDummy266 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy265 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy266 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0272 (A : SemanticCore.Class) : nb090AlphaDummy262 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy262 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy263 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0273 (h : SemanticCore.Var) : nb090AlphaDummy265 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy265 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy266 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0274 (A : SemanticCore.Class) : nb090AlphaDummy262 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy262 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy262 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0275 (h : SemanticCore.Var) : nb090AlphaDummy265 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy265 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy265 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0276 (A : SemanticCore.Class) : nb090AlphaDummy263 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy262 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy263 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0277 (h : SemanticCore.Var) : nb090AlphaDummy266 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy265 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy266 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0278 (A : SemanticCore.Class) : nb090AlphaDummy263 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy263 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy263 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0279 (h : SemanticCore.Var) : nb090AlphaDummy266 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy266 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy266 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0280 (A : SemanticCore.Class) : nb090AlphaDummy243 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy244 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy243 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0281 (A : SemanticCore.Class) : nb090AlphaDummy243 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy247 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy248 A) (SemanticCore.Class.cv (nb090AlphaDummy244 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy247 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy247 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy248 A) (SemanticCore.Class.cv (nb090AlphaDummy243 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy247 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0282 (h : SemanticCore.Var) : nb090AlphaDummy245 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy246 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy245 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0283 (h : SemanticCore.Var) : nb090AlphaDummy245 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy249 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy250 h) (SemanticCore.Class.cv (nb090AlphaDummy246 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy249 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy249 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy250 h) (SemanticCore.Class.cv (nb090AlphaDummy245 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy249 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0284 (A : SemanticCore.Class) : nb090AlphaDummy243 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy247 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy248 A) (SemanticCore.Class.cv (nb090AlphaDummy243 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy247 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy247 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy248 A) (SemanticCore.Class.cv (nb090AlphaDummy243 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy247 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0285 (h : SemanticCore.Var) : nb090AlphaDummy245 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy249 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy250 h) (SemanticCore.Class.cv (nb090AlphaDummy245 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy249 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy249 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy250 h) (SemanticCore.Class.cv (nb090AlphaDummy245 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy249 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0286 (A : SemanticCore.Class) : nb090AlphaDummy248 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0287 (h : SemanticCore.Var) : nb090AlphaDummy250 h ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0288 (A : SemanticCore.Class) : nb090AlphaDummy248 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0289 (h : SemanticCore.Var) : nb090AlphaDummy250 h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0290 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0291 (h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0292 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ Compiler.CompactSourceSyntax.synC2nd.fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy001 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0293 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ {nb090AlphaDummy283 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy001 A)) Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy283 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0294 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy285 A) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy283 A) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy001 A)) Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy283 A)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy285 A))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0295 (u : SemanticCore.Var) : u ∈ Compiler.CompactSourceSyntax.synC2nd.fv ∪ (SemanticCore.Class.cv u).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0296 (u : SemanticCore.Var) : u ∈ {nb090AlphaDummy284 u} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy284 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0297 (u : SemanticCore.Var) : u ∈ (SemanticCore.Class.cab (nb090AlphaDummy286 u) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy284 u) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy284 u)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy286 u))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0298 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy001 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy283 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0299 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy291 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy292 A) (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy291 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy291 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy292 A) (SemanticCore.Class.cv (nb090AlphaDummy283 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy291 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0300 (u : SemanticCore.Var) : u ∈ (SemanticCore.Class.cv u).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy284 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0301 (u : SemanticCore.Var) : u ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy293 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy294 u) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy293 u)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy293 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy294 u) (SemanticCore.Class.cv (nb090AlphaDummy284 u)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy293 u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0302 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy291 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy292 A) (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy291 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy291 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy292 A) (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy291 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0303 (u : SemanticCore.Var) : u ∈ (SemanticCore.Class.cab (nb090AlphaDummy293 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy294 u) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy293 u)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy293 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy294 u) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy293 u)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0304 (A : SemanticCore.Class) : nb090AlphaDummy292 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy292 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0305 (u : SemanticCore.Var) : nb090AlphaDummy294 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy294 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0306 (A : SemanticCore.Class) : nb090AlphaDummy299 A ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy299 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy299 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy299 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0307 (u : SemanticCore.Var) : nb090AlphaDummy301 u ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy301 u)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy301 u)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy301 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0308 (A : SemanticCore.Class) : nb090AlphaDummy299 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy299 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0309 (u : SemanticCore.Var) : nb090AlphaDummy301 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy301 u)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0310 (A : SemanticCore.Class) : nb090AlphaDummy306 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy306 A)) (SemanticCore.Class.cv (nb090AlphaDummy307 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy306 A)) (SemanticCore.Class.cv (nb090AlphaDummy307 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0311 (u : SemanticCore.Var) : nb090AlphaDummy309 u ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy309 u)) (SemanticCore.Class.cv (nb090AlphaDummy310 u))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy309 u)) (SemanticCore.Class.cv (nb090AlphaDummy310 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0312 (A : SemanticCore.Class) : nb090AlphaDummy306 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy306 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy307 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0313 (u : SemanticCore.Var) : nb090AlphaDummy309 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy309 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy310 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0314 (A : SemanticCore.Class) : nb090AlphaDummy307 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy306 A)) (SemanticCore.Class.cv (nb090AlphaDummy307 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy306 A)) (SemanticCore.Class.cv (nb090AlphaDummy307 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0315 (u : SemanticCore.Var) : nb090AlphaDummy310 u ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy309 u)) (SemanticCore.Class.cv (nb090AlphaDummy310 u))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy309 u)) (SemanticCore.Class.cv (nb090AlphaDummy310 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0316 (A : SemanticCore.Class) : nb090AlphaDummy307 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy306 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy307 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0317 (u : SemanticCore.Var) : nb090AlphaDummy310 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy309 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy310 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0318 (A : SemanticCore.Class) : nb090AlphaDummy306 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy306 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy307 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0319 (u : SemanticCore.Var) : nb090AlphaDummy309 u ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy309 u))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy310 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0320 (A : SemanticCore.Class) : nb090AlphaDummy306 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy306 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy306 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0321 (u : SemanticCore.Var) : nb090AlphaDummy309 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy309 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy309 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0322 (A : SemanticCore.Class) : nb090AlphaDummy307 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy306 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy307 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0323 (u : SemanticCore.Var) : nb090AlphaDummy310 u ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy309 u))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy310 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0324 (A : SemanticCore.Class) : nb090AlphaDummy307 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy307 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy307 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0325 (u : SemanticCore.Var) : nb090AlphaDummy310 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy310 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy310 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0326 (A : SemanticCore.Class) : nb090AlphaDummy283 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy001 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy283 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0327 (A : SemanticCore.Class) : nb090AlphaDummy283 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy291 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy292 A) (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy291 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy291 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy292 A) (SemanticCore.Class.cv (nb090AlphaDummy283 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy291 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0328 (u : SemanticCore.Var) : nb090AlphaDummy284 u ∈ (SemanticCore.Class.cv u).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy284 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0329 (u : SemanticCore.Var) : nb090AlphaDummy284 u ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy293 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy294 u) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy293 u)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy293 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy294 u) (SemanticCore.Class.cv (nb090AlphaDummy284 u)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy293 u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0330 (A : SemanticCore.Class) : nb090AlphaDummy283 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy291 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy292 A) (SemanticCore.Class.cv (nb090AlphaDummy283 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy291 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy291 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy292 A) (SemanticCore.Class.cv (nb090AlphaDummy283 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy291 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0331 (u : SemanticCore.Var) : nb090AlphaDummy284 u ∈ (SemanticCore.Class.cab (nb090AlphaDummy293 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy294 u) (SemanticCore.Class.cv (nb090AlphaDummy284 u)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy293 u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy293 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy294 u) (SemanticCore.Class.cv (nb090AlphaDummy284 u)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy293 u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0332 (A : SemanticCore.Class) : nb090AlphaDummy292 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0333 (u : SemanticCore.Var) : nb090AlphaDummy294 u ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0334 (A : SemanticCore.Class) : nb090AlphaDummy292 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0335 (u : SemanticCore.Var) : nb090AlphaDummy294 u ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0336 (A : SemanticCore.Class) : nb090AlphaDummy285 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy285 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0337 (u : SemanticCore.Var) : nb090AlphaDummy286 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy286 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0338 (A : SemanticCore.Class) : nb090AlphaDummy334 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy334 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy333 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0339 (A : SemanticCore.Class) : nb090AlphaDummy334 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy337 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy338 A) (SemanticCore.Class.cv (nb090AlphaDummy334 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy337 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy337 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy338 A) (SemanticCore.Class.cv (nb090AlphaDummy333 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy337 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0340 (h : SemanticCore.Var) : nb090AlphaDummy336 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy336 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy335 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0341 (h : SemanticCore.Var) : nb090AlphaDummy336 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy339 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy340 h) (SemanticCore.Class.cv (nb090AlphaDummy336 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy339 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy339 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy340 h) (SemanticCore.Class.cv (nb090AlphaDummy335 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy339 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0342 (A : SemanticCore.Class) : nb090AlphaDummy334 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy337 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy338 A) (SemanticCore.Class.cv (nb090AlphaDummy334 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy337 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy337 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy338 A) (SemanticCore.Class.cv (nb090AlphaDummy334 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy337 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0343 (h : SemanticCore.Var) : nb090AlphaDummy336 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy339 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy340 h) (SemanticCore.Class.cv (nb090AlphaDummy336 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy339 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy339 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy340 h) (SemanticCore.Class.cv (nb090AlphaDummy336 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy339 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0344 (A : SemanticCore.Class) : nb090AlphaDummy338 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy338 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0345 (h : SemanticCore.Var) : nb090AlphaDummy340 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy340 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0346 (A : SemanticCore.Class) : nb090AlphaDummy345 A ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy345 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy345 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy345 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0347 (h : SemanticCore.Var) : nb090AlphaDummy347 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy347 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy347 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy347 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0348 (A : SemanticCore.Class) : nb090AlphaDummy345 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy345 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0349 (h : SemanticCore.Var) : nb090AlphaDummy347 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy347 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0350 (A : SemanticCore.Class) : nb090AlphaDummy352 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy352 A)) (SemanticCore.Class.cv (nb090AlphaDummy353 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy352 A)) (SemanticCore.Class.cv (nb090AlphaDummy353 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0351 (h : SemanticCore.Var) : nb090AlphaDummy355 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy355 h)) (SemanticCore.Class.cv (nb090AlphaDummy356 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy355 h)) (SemanticCore.Class.cv (nb090AlphaDummy356 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0352 (A : SemanticCore.Class) : nb090AlphaDummy352 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy352 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy353 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0353 (h : SemanticCore.Var) : nb090AlphaDummy355 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy355 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy356 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0354 (A : SemanticCore.Class) : nb090AlphaDummy353 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy352 A)) (SemanticCore.Class.cv (nb090AlphaDummy353 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy352 A)) (SemanticCore.Class.cv (nb090AlphaDummy353 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0355 (h : SemanticCore.Var) : nb090AlphaDummy356 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy355 h)) (SemanticCore.Class.cv (nb090AlphaDummy356 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy355 h)) (SemanticCore.Class.cv (nb090AlphaDummy356 h))).fv

Certificates from NAR4C090C001Part018.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0356 (A : SemanticCore.Class) : nb090AlphaDummy353 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy352 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy353 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0357 (h : SemanticCore.Var) : nb090AlphaDummy356 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy355 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy356 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0358 (A : SemanticCore.Class) : nb090AlphaDummy352 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy352 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy353 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0359 (h : SemanticCore.Var) : nb090AlphaDummy355 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy355 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy356 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0360 (A : SemanticCore.Class) : nb090AlphaDummy352 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy352 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy352 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0361 (h : SemanticCore.Var) : nb090AlphaDummy355 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy355 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy355 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0362 (A : SemanticCore.Class) : nb090AlphaDummy353 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy352 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy353 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0363 (h : SemanticCore.Var) : nb090AlphaDummy356 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy355 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy356 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0364 (A : SemanticCore.Class) : nb090AlphaDummy353 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy353 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy353 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0365 (h : SemanticCore.Var) : nb090AlphaDummy356 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy356 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy356 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0366 (A : SemanticCore.Class) : nb090AlphaDummy333 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy334 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy333 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0367 (A : SemanticCore.Class) : nb090AlphaDummy333 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy337 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy338 A) (SemanticCore.Class.cv (nb090AlphaDummy334 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy337 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy337 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy338 A) (SemanticCore.Class.cv (nb090AlphaDummy333 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy337 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0368 (h : SemanticCore.Var) : nb090AlphaDummy335 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy336 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy335 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0369 (h : SemanticCore.Var) : nb090AlphaDummy335 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy339 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy340 h) (SemanticCore.Class.cv (nb090AlphaDummy336 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy339 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy339 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy340 h) (SemanticCore.Class.cv (nb090AlphaDummy335 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy339 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0370 (A : SemanticCore.Class) : nb090AlphaDummy333 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy337 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy338 A) (SemanticCore.Class.cv (nb090AlphaDummy333 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy337 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy337 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy338 A) (SemanticCore.Class.cv (nb090AlphaDummy333 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy337 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0371 (h : SemanticCore.Var) : nb090AlphaDummy335 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy339 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy340 h) (SemanticCore.Class.cv (nb090AlphaDummy335 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy339 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy339 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy340 h) (SemanticCore.Class.cv (nb090AlphaDummy335 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy339 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0372 (A : SemanticCore.Class) : nb090AlphaDummy338 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0373 (h : SemanticCore.Var) : nb090AlphaDummy340 h ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0374 (A : SemanticCore.Class) : nb090AlphaDummy338 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0375 (h : SemanticCore.Var) : nb090AlphaDummy340 h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0376 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0377 (v h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0378 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0379 (v h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0380 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy000 A)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0381 (h : SemanticCore.Var) : h ∈ (SemanticCore.Class.cv h).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0382 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0383 (v h : SemanticCore.Var) : v ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0384 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0385 (v h : SemanticCore.Var) : v ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0386 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ Compiler.CompactSourceSyntax.synC2nd.fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy002 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0387 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ {nb090AlphaDummy373 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy002 A)) Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy373 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0388 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy375 A) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy373 A) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy002 A)) Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy373 A)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy375 A))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0389 (v : SemanticCore.Var) : v ∈ Compiler.CompactSourceSyntax.synC2nd.fv ∪ (SemanticCore.Class.cv v).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0390 (v : SemanticCore.Var) : v ∈ {nb090AlphaDummy374 v} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv v) Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy374 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0391 (v : SemanticCore.Var) : v ∈ (SemanticCore.Class.cab (nb090AlphaDummy376 v) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy374 v) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv v) Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy374 v)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy376 v))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0392 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy002 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy373 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0393 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy381 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy382 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy381 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy381 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy382 A) (SemanticCore.Class.cv (nb090AlphaDummy373 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy381 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0394 (v : SemanticCore.Var) : v ∈ (SemanticCore.Class.cv v).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy374 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0395 (v : SemanticCore.Var) : v ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy383 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy384 v) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy383 v)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy383 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy384 v) (SemanticCore.Class.cv (nb090AlphaDummy374 v)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy383 v)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0396 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy381 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy382 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy381 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy381 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy382 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy381 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0397 (v : SemanticCore.Var) : v ∈ (SemanticCore.Class.cab (nb090AlphaDummy383 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy384 v) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy383 v)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy383 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy384 v) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy383 v)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0398 (A : SemanticCore.Class) : nb090AlphaDummy382 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy382 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0399 (v : SemanticCore.Var) : nb090AlphaDummy384 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy384 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0400 (A : SemanticCore.Class) : nb090AlphaDummy389 A ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy389 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy389 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy389 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0401 (v : SemanticCore.Var) : nb090AlphaDummy391 v ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy391 v)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy391 v)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy391 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0402 (A : SemanticCore.Class) : nb090AlphaDummy389 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy389 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0403 (v : SemanticCore.Var) : nb090AlphaDummy391 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy391 v)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0404 (A : SemanticCore.Class) : nb090AlphaDummy396 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy396 A)) (SemanticCore.Class.cv (nb090AlphaDummy397 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy396 A)) (SemanticCore.Class.cv (nb090AlphaDummy397 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0405 (v : SemanticCore.Var) : nb090AlphaDummy399 v ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy399 v)) (SemanticCore.Class.cv (nb090AlphaDummy400 v))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy399 v)) (SemanticCore.Class.cv (nb090AlphaDummy400 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0406 (A : SemanticCore.Class) : nb090AlphaDummy396 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy396 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy397 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0407 (v : SemanticCore.Var) : nb090AlphaDummy399 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy399 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy400 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0408 (A : SemanticCore.Class) : nb090AlphaDummy397 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy396 A)) (SemanticCore.Class.cv (nb090AlphaDummy397 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy396 A)) (SemanticCore.Class.cv (nb090AlphaDummy397 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0409 (v : SemanticCore.Var) : nb090AlphaDummy400 v ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy399 v)) (SemanticCore.Class.cv (nb090AlphaDummy400 v))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy399 v)) (SemanticCore.Class.cv (nb090AlphaDummy400 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0410 (A : SemanticCore.Class) : nb090AlphaDummy397 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy396 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy397 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0411 (v : SemanticCore.Var) : nb090AlphaDummy400 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy399 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy400 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0412 (A : SemanticCore.Class) : nb090AlphaDummy396 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy396 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy397 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0413 (v : SemanticCore.Var) : nb090AlphaDummy399 v ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy399 v))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy400 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0414 (A : SemanticCore.Class) : nb090AlphaDummy396 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy396 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy396 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0415 (v : SemanticCore.Var) : nb090AlphaDummy399 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy399 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy399 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0416 (A : SemanticCore.Class) : nb090AlphaDummy397 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy396 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy397 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0417 (v : SemanticCore.Var) : nb090AlphaDummy400 v ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy399 v))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy400 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0418 (A : SemanticCore.Class) : nb090AlphaDummy397 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy397 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy397 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0419 (v : SemanticCore.Var) : nb090AlphaDummy400 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy400 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy400 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0420 (A : SemanticCore.Class) : nb090AlphaDummy373 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy002 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy373 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0421 (A : SemanticCore.Class) : nb090AlphaDummy373 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy381 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy382 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy381 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy381 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy382 A) (SemanticCore.Class.cv (nb090AlphaDummy373 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy381 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0422 (v : SemanticCore.Var) : nb090AlphaDummy374 v ∈ (SemanticCore.Class.cv v).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy374 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0423 (v : SemanticCore.Var) : nb090AlphaDummy374 v ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy383 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy384 v) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy383 v)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy383 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy384 v) (SemanticCore.Class.cv (nb090AlphaDummy374 v)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy383 v)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0424 (A : SemanticCore.Class) : nb090AlphaDummy373 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy381 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy382 A) (SemanticCore.Class.cv (nb090AlphaDummy373 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy381 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy381 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy382 A) (SemanticCore.Class.cv (nb090AlphaDummy373 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy381 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0425 (v : SemanticCore.Var) : nb090AlphaDummy374 v ∈ (SemanticCore.Class.cab (nb090AlphaDummy383 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy384 v) (SemanticCore.Class.cv (nb090AlphaDummy374 v)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy383 v)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy383 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy384 v) (SemanticCore.Class.cv (nb090AlphaDummy374 v)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy383 v)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0426 (A : SemanticCore.Class) : nb090AlphaDummy382 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0427 (v : SemanticCore.Var) : nb090AlphaDummy384 v ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0428 (A : SemanticCore.Class) : nb090AlphaDummy382 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0429 (v : SemanticCore.Var) : nb090AlphaDummy384 v ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0430 (A : SemanticCore.Class) : nb090AlphaDummy375 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy375 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0431 (v : SemanticCore.Var) : nb090AlphaDummy376 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy376 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0432 (A : SemanticCore.Class) : nb090AlphaDummy423 A ∈ {nb090AlphaDummy423 A} ∪ {nb090AlphaDummy424 A} ∪ (Compiler.CompactSourceSyntax.synWex (nb090AlphaDummy425 A) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy423 A)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A)))) (SemanticCore.Class.cv (nb090AlphaDummy425 A))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy425 A)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (SemanticCore.Class.cv (nb090AlphaDummy424 A))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0433 (h : SemanticCore.Var) : nb090AlphaDummy426 h ∈ {nb090AlphaDummy426 h} ∪ {nb090AlphaDummy427 h} ∪ (Compiler.CompactSourceSyntax.synWex (nb090AlphaDummy428 h) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy426 h)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h))) (SemanticCore.Class.cv (nb090AlphaDummy428 h))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy428 h)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (SemanticCore.Class.cv (nb090AlphaDummy427 h))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0434 (A : SemanticCore.Class) : nb090AlphaDummy424 A ∈ {nb090AlphaDummy423 A} ∪ {nb090AlphaDummy424 A} ∪ (Compiler.CompactSourceSyntax.synWex (nb090AlphaDummy425 A) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy423 A)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A)))) (SemanticCore.Class.cv (nb090AlphaDummy425 A))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy425 A)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (SemanticCore.Class.cv (nb090AlphaDummy424 A))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0435 (h : SemanticCore.Var) : nb090AlphaDummy427 h ∈ {nb090AlphaDummy426 h} ∪ {nb090AlphaDummy427 h} ∪ (Compiler.CompactSourceSyntax.synWex (nb090AlphaDummy428 h) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy426 h)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h))) (SemanticCore.Class.cv (nb090AlphaDummy428 h))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy428 h)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (SemanticCore.Class.cv (nb090AlphaDummy427 h))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0436 (A : SemanticCore.Class) : nb090AlphaDummy423 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy423 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy424 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0437 (A : SemanticCore.Class) : nb090AlphaDummy423 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy431 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy432 A) (SemanticCore.Class.cv (nb090AlphaDummy423 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy431 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy431 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy432 A) (SemanticCore.Class.cv (nb090AlphaDummy424 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy431 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0438 (h : SemanticCore.Var) : nb090AlphaDummy426 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy426 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy427 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0439 (h : SemanticCore.Var) : nb090AlphaDummy426 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy433 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy434 h) (SemanticCore.Class.cv (nb090AlphaDummy426 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy433 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy433 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy434 h) (SemanticCore.Class.cv (nb090AlphaDummy427 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy433 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0440 (A : SemanticCore.Class) : nb090AlphaDummy423 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy431 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy432 A) (SemanticCore.Class.cv (nb090AlphaDummy423 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy431 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy431 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy432 A) (SemanticCore.Class.cv (nb090AlphaDummy423 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy431 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0441 (h : SemanticCore.Var) : nb090AlphaDummy426 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy433 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy434 h) (SemanticCore.Class.cv (nb090AlphaDummy426 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy433 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy433 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy434 h) (SemanticCore.Class.cv (nb090AlphaDummy426 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy433 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0442 (A : SemanticCore.Class) : nb090AlphaDummy432 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy432 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0443 (h : SemanticCore.Var) : nb090AlphaDummy434 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy434 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0444 (A : SemanticCore.Class) : nb090AlphaDummy439 A ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy439 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy439 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy439 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0445 (h : SemanticCore.Var) : nb090AlphaDummy441 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy441 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy441 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy441 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0446 (A : SemanticCore.Class) : nb090AlphaDummy439 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy439 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0447 (h : SemanticCore.Var) : nb090AlphaDummy441 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy441 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0448 (A : SemanticCore.Class) : nb090AlphaDummy446 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy446 A)) (SemanticCore.Class.cv (nb090AlphaDummy447 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy446 A)) (SemanticCore.Class.cv (nb090AlphaDummy447 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0449 (h : SemanticCore.Var) : nb090AlphaDummy449 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy449 h)) (SemanticCore.Class.cv (nb090AlphaDummy450 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy449 h)) (SemanticCore.Class.cv (nb090AlphaDummy450 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0450 (A : SemanticCore.Class) : nb090AlphaDummy446 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy446 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy447 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0451 (h : SemanticCore.Var) : nb090AlphaDummy449 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy449 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy450 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0452 (A : SemanticCore.Class) : nb090AlphaDummy447 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy446 A)) (SemanticCore.Class.cv (nb090AlphaDummy447 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy446 A)) (SemanticCore.Class.cv (nb090AlphaDummy447 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0453 (h : SemanticCore.Var) : nb090AlphaDummy450 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy449 h)) (SemanticCore.Class.cv (nb090AlphaDummy450 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy449 h)) (SemanticCore.Class.cv (nb090AlphaDummy450 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0454 (A : SemanticCore.Class) : nb090AlphaDummy447 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy446 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy447 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0455 (h : SemanticCore.Var) : nb090AlphaDummy450 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy449 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy450 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0456 (A : SemanticCore.Class) : nb090AlphaDummy446 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy446 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy447 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0457 (h : SemanticCore.Var) : nb090AlphaDummy449 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy449 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy450 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0458 (A : SemanticCore.Class) : nb090AlphaDummy446 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy446 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy446 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0459 (h : SemanticCore.Var) : nb090AlphaDummy449 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy449 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy449 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0460 (A : SemanticCore.Class) : nb090AlphaDummy447 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy446 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy447 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0461 (h : SemanticCore.Var) : nb090AlphaDummy450 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy449 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy450 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0462 (A : SemanticCore.Class) : nb090AlphaDummy447 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy447 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy447 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0463 (h : SemanticCore.Var) : nb090AlphaDummy450 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy450 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy450 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0464 (A : SemanticCore.Class) : nb090AlphaDummy424 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy423 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy424 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0465 (A : SemanticCore.Class) : nb090AlphaDummy424 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy431 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy432 A) (SemanticCore.Class.cv (nb090AlphaDummy423 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy431 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy431 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy432 A) (SemanticCore.Class.cv (nb090AlphaDummy424 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy431 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0466 (h : SemanticCore.Var) : nb090AlphaDummy427 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy426 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy427 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0467 (h : SemanticCore.Var) : nb090AlphaDummy427 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy433 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy434 h) (SemanticCore.Class.cv (nb090AlphaDummy426 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy433 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy433 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy434 h) (SemanticCore.Class.cv (nb090AlphaDummy427 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy433 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0468 (A : SemanticCore.Class) : nb090AlphaDummy424 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy431 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy432 A) (SemanticCore.Class.cv (nb090AlphaDummy424 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy431 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy431 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy432 A) (SemanticCore.Class.cv (nb090AlphaDummy424 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy431 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0469 (h : SemanticCore.Var) : nb090AlphaDummy427 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy433 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy434 h) (SemanticCore.Class.cv (nb090AlphaDummy427 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy433 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy433 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy434 h) (SemanticCore.Class.cv (nb090AlphaDummy427 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy433 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0470 (A : SemanticCore.Class) : nb090AlphaDummy432 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0471 (h : SemanticCore.Var) : nb090AlphaDummy434 h ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0472 (A : SemanticCore.Class) : nb090AlphaDummy432 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0473 (h : SemanticCore.Var) : nb090AlphaDummy434 h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0474 (A : SemanticCore.Class) : nb090AlphaDummy423 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy423 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy425 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0475 (A : SemanticCore.Class) : nb090AlphaDummy423 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy467 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy468 A) (SemanticCore.Class.cv (nb090AlphaDummy423 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy467 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy467 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy468 A) (SemanticCore.Class.cv (nb090AlphaDummy425 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy467 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0476 (h : SemanticCore.Var) : nb090AlphaDummy426 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy426 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy428 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0477 (h : SemanticCore.Var) : nb090AlphaDummy426 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy469 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy470 h) (SemanticCore.Class.cv (nb090AlphaDummy426 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy469 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy469 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy470 h) (SemanticCore.Class.cv (nb090AlphaDummy428 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy469 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0478 (A : SemanticCore.Class) : nb090AlphaDummy423 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy467 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy468 A) (SemanticCore.Class.cv (nb090AlphaDummy423 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy467 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy467 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy468 A) (SemanticCore.Class.cv (nb090AlphaDummy423 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy467 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0479 (h : SemanticCore.Var) : nb090AlphaDummy426 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy469 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy470 h) (SemanticCore.Class.cv (nb090AlphaDummy426 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy469 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy469 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy470 h) (SemanticCore.Class.cv (nb090AlphaDummy426 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy469 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0480 (A : SemanticCore.Class) : nb090AlphaDummy468 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy468 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0481 (h : SemanticCore.Var) : nb090AlphaDummy470 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy470 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0482 (A : SemanticCore.Class) : nb090AlphaDummy475 A ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy475 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy475 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy475 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0483 (h : SemanticCore.Var) : nb090AlphaDummy477 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy477 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy477 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy477 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0484 (A : SemanticCore.Class) : nb090AlphaDummy475 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy475 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0485 (h : SemanticCore.Var) : nb090AlphaDummy477 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy477 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0486 (A : SemanticCore.Class) : nb090AlphaDummy482 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy482 A)) (SemanticCore.Class.cv (nb090AlphaDummy483 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy482 A)) (SemanticCore.Class.cv (nb090AlphaDummy483 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0487 (h : SemanticCore.Var) : nb090AlphaDummy485 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy485 h)) (SemanticCore.Class.cv (nb090AlphaDummy486 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy485 h)) (SemanticCore.Class.cv (nb090AlphaDummy486 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0488 (A : SemanticCore.Class) : nb090AlphaDummy482 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy482 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy483 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0489 (h : SemanticCore.Var) : nb090AlphaDummy485 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy485 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy486 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0490 (A : SemanticCore.Class) : nb090AlphaDummy483 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy482 A)) (SemanticCore.Class.cv (nb090AlphaDummy483 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy482 A)) (SemanticCore.Class.cv (nb090AlphaDummy483 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0491 (h : SemanticCore.Var) : nb090AlphaDummy486 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy485 h)) (SemanticCore.Class.cv (nb090AlphaDummy486 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy485 h)) (SemanticCore.Class.cv (nb090AlphaDummy486 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0492 (A : SemanticCore.Class) : nb090AlphaDummy483 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy482 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy483 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0493 (h : SemanticCore.Var) : nb090AlphaDummy486 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy485 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy486 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0494 (A : SemanticCore.Class) : nb090AlphaDummy482 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy482 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy483 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0495 (h : SemanticCore.Var) : nb090AlphaDummy485 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy485 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy486 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0496 (A : SemanticCore.Class) : nb090AlphaDummy482 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy482 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy482 A)).fv

Certificates from NAR4C090C001Part019.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0497 (h : SemanticCore.Var) : nb090AlphaDummy485 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy485 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy485 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0498 (A : SemanticCore.Class) : nb090AlphaDummy483 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy482 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy483 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0499 (h : SemanticCore.Var) : nb090AlphaDummy486 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy485 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy486 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0500 (A : SemanticCore.Class) : nb090AlphaDummy483 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy483 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy483 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0501 (h : SemanticCore.Var) : nb090AlphaDummy486 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy486 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy486 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0502 (A : SemanticCore.Class) : nb090AlphaDummy425 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy423 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy425 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0503 (A : SemanticCore.Class) : nb090AlphaDummy425 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy467 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy468 A) (SemanticCore.Class.cv (nb090AlphaDummy423 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy467 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy467 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy468 A) (SemanticCore.Class.cv (nb090AlphaDummy425 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy467 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0504 (h : SemanticCore.Var) : nb090AlphaDummy428 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy426 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy428 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0505 (h : SemanticCore.Var) : nb090AlphaDummy428 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy469 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy470 h) (SemanticCore.Class.cv (nb090AlphaDummy426 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy469 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy469 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy470 h) (SemanticCore.Class.cv (nb090AlphaDummy428 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy469 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0506 (A : SemanticCore.Class) : nb090AlphaDummy425 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy467 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy468 A) (SemanticCore.Class.cv (nb090AlphaDummy425 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy467 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy467 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy468 A) (SemanticCore.Class.cv (nb090AlphaDummy425 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy467 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0507 (h : SemanticCore.Var) : nb090AlphaDummy428 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy469 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy470 h) (SemanticCore.Class.cv (nb090AlphaDummy428 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy469 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy469 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy470 h) (SemanticCore.Class.cv (nb090AlphaDummy428 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy469 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0508 (A : SemanticCore.Class) : nb090AlphaDummy468 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0509 (h : SemanticCore.Var) : nb090AlphaDummy470 h ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0510 (A : SemanticCore.Class) : nb090AlphaDummy468 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0511 (h : SemanticCore.Var) : nb090AlphaDummy470 h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0512 (A : SemanticCore.Class) : nb090AlphaDummy503 A ∈ {nb090AlphaDummy503 A} ∪ {nb090AlphaDummy504 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (SemanticCore.Class.cv (nb090AlphaDummy503 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0513 (h : SemanticCore.Var) : nb090AlphaDummy505 h ∈ {nb090AlphaDummy505 h} ∪ {nb090AlphaDummy506 h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (SemanticCore.Class.cv (nb090AlphaDummy505 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0514 (A : SemanticCore.Class) : nb090AlphaDummy504 A ∈ {nb090AlphaDummy503 A} ∪ {nb090AlphaDummy504 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (SemanticCore.Class.cv (nb090AlphaDummy503 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0515 (h : SemanticCore.Var) : nb090AlphaDummy506 h ∈ {nb090AlphaDummy505 h} ∪ {nb090AlphaDummy506 h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (SemanticCore.Class.cv (nb090AlphaDummy505 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0516 (A : SemanticCore.Class) : nb090AlphaDummy503 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy503 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy504 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0517 (A : SemanticCore.Class) : nb090AlphaDummy503 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy509 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy510 A) (SemanticCore.Class.cv (nb090AlphaDummy503 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy509 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy509 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy510 A) (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy509 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0518 (h : SemanticCore.Var) : nb090AlphaDummy505 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy505 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy506 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0519 (h : SemanticCore.Var) : nb090AlphaDummy505 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy511 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy512 h) (SemanticCore.Class.cv (nb090AlphaDummy505 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy511 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy511 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy512 h) (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy511 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0520 (A : SemanticCore.Class) : nb090AlphaDummy503 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy509 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy510 A) (SemanticCore.Class.cv (nb090AlphaDummy503 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy509 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy509 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy510 A) (SemanticCore.Class.cv (nb090AlphaDummy503 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy509 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0521 (h : SemanticCore.Var) : nb090AlphaDummy505 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy511 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy512 h) (SemanticCore.Class.cv (nb090AlphaDummy505 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy511 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy511 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy512 h) (SemanticCore.Class.cv (nb090AlphaDummy505 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy511 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0522 (A : SemanticCore.Class) : nb090AlphaDummy510 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy510 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0523 (h : SemanticCore.Var) : nb090AlphaDummy512 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy512 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0524 (A : SemanticCore.Class) : nb090AlphaDummy517 A ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy517 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy517 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy517 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0525 (h : SemanticCore.Var) : nb090AlphaDummy519 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy519 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy519 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy519 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0526 (A : SemanticCore.Class) : nb090AlphaDummy517 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy517 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0527 (h : SemanticCore.Var) : nb090AlphaDummy519 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy519 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0528 (A : SemanticCore.Class) : nb090AlphaDummy524 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy524 A)) (SemanticCore.Class.cv (nb090AlphaDummy525 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy524 A)) (SemanticCore.Class.cv (nb090AlphaDummy525 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0529 (h : SemanticCore.Var) : nb090AlphaDummy527 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy527 h)) (SemanticCore.Class.cv (nb090AlphaDummy528 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy527 h)) (SemanticCore.Class.cv (nb090AlphaDummy528 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0530 (A : SemanticCore.Class) : nb090AlphaDummy524 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy524 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy525 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0531 (h : SemanticCore.Var) : nb090AlphaDummy527 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy527 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy528 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0532 (A : SemanticCore.Class) : nb090AlphaDummy525 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy524 A)) (SemanticCore.Class.cv (nb090AlphaDummy525 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy524 A)) (SemanticCore.Class.cv (nb090AlphaDummy525 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0533 (h : SemanticCore.Var) : nb090AlphaDummy528 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy527 h)) (SemanticCore.Class.cv (nb090AlphaDummy528 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy527 h)) (SemanticCore.Class.cv (nb090AlphaDummy528 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0534 (A : SemanticCore.Class) : nb090AlphaDummy525 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy524 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy525 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0535 (h : SemanticCore.Var) : nb090AlphaDummy528 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy527 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy528 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0536 (A : SemanticCore.Class) : nb090AlphaDummy524 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy524 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy525 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0537 (h : SemanticCore.Var) : nb090AlphaDummy527 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy527 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy528 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0538 (A : SemanticCore.Class) : nb090AlphaDummy524 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy524 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy524 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0539 (h : SemanticCore.Var) : nb090AlphaDummy527 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy527 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy527 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0540 (A : SemanticCore.Class) : nb090AlphaDummy525 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy524 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy525 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0541 (h : SemanticCore.Var) : nb090AlphaDummy528 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy527 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy528 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0542 (A : SemanticCore.Class) : nb090AlphaDummy525 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy525 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy525 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0543 (h : SemanticCore.Var) : nb090AlphaDummy528 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy528 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy528 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0544 (A : SemanticCore.Class) : nb090AlphaDummy504 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy503 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy504 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0545 (A : SemanticCore.Class) : nb090AlphaDummy504 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy509 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy510 A) (SemanticCore.Class.cv (nb090AlphaDummy503 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy509 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy509 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy510 A) (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy509 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0546 (h : SemanticCore.Var) : nb090AlphaDummy506 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy505 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy506 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0547 (h : SemanticCore.Var) : nb090AlphaDummy506 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy511 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy512 h) (SemanticCore.Class.cv (nb090AlphaDummy505 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy511 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy511 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy512 h) (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy511 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0548 (A : SemanticCore.Class) : nb090AlphaDummy504 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy509 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy510 A) (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy509 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy509 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy510 A) (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy509 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0549 (h : SemanticCore.Var) : nb090AlphaDummy506 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy511 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy512 h) (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy511 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy511 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy512 h) (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy511 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0550 (A : SemanticCore.Class) : nb090AlphaDummy510 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0551 (h : SemanticCore.Var) : nb090AlphaDummy512 h ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0552 (A : SemanticCore.Class) : nb090AlphaDummy510 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0553 (h : SemanticCore.Var) : nb090AlphaDummy512 h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0554 (A : SemanticCore.Class) : nb090AlphaDummy504 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy504 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy503 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0555 (A : SemanticCore.Class) : nb090AlphaDummy504 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy545 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy546 A) (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy545 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy545 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy546 A) (SemanticCore.Class.cv (nb090AlphaDummy503 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy545 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0556 (h : SemanticCore.Var) : nb090AlphaDummy506 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy506 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy505 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0557 (h : SemanticCore.Var) : nb090AlphaDummy506 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy547 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy548 h) (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy547 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy547 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy548 h) (SemanticCore.Class.cv (nb090AlphaDummy505 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy547 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0558 (A : SemanticCore.Class) : nb090AlphaDummy504 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy545 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy546 A) (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy545 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy545 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy546 A) (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy545 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0559 (h : SemanticCore.Var) : nb090AlphaDummy506 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy547 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy548 h) (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy547 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy547 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy548 h) (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy547 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0560 (A : SemanticCore.Class) : nb090AlphaDummy546 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy546 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0561 (h : SemanticCore.Var) : nb090AlphaDummy548 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy548 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0562 (A : SemanticCore.Class) : nb090AlphaDummy553 A ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy553 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy553 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy553 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0563 (h : SemanticCore.Var) : nb090AlphaDummy555 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy555 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy555 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy555 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0564 (A : SemanticCore.Class) : nb090AlphaDummy553 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy553 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0565 (h : SemanticCore.Var) : nb090AlphaDummy555 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy555 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0566 (A : SemanticCore.Class) : nb090AlphaDummy560 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy560 A)) (SemanticCore.Class.cv (nb090AlphaDummy561 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy560 A)) (SemanticCore.Class.cv (nb090AlphaDummy561 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0567 (h : SemanticCore.Var) : nb090AlphaDummy563 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy563 h)) (SemanticCore.Class.cv (nb090AlphaDummy564 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy563 h)) (SemanticCore.Class.cv (nb090AlphaDummy564 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0568 (A : SemanticCore.Class) : nb090AlphaDummy560 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy560 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy561 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0569 (h : SemanticCore.Var) : nb090AlphaDummy563 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy563 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy564 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0570 (A : SemanticCore.Class) : nb090AlphaDummy561 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy560 A)) (SemanticCore.Class.cv (nb090AlphaDummy561 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy560 A)) (SemanticCore.Class.cv (nb090AlphaDummy561 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0571 (h : SemanticCore.Var) : nb090AlphaDummy564 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy563 h)) (SemanticCore.Class.cv (nb090AlphaDummy564 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy563 h)) (SemanticCore.Class.cv (nb090AlphaDummy564 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0572 (A : SemanticCore.Class) : nb090AlphaDummy561 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy560 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy561 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0573 (h : SemanticCore.Var) : nb090AlphaDummy564 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy563 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy564 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0574 (A : SemanticCore.Class) : nb090AlphaDummy560 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy560 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy561 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0575 (h : SemanticCore.Var) : nb090AlphaDummy563 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy563 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy564 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0576 (A : SemanticCore.Class) : nb090AlphaDummy560 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy560 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy560 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0577 (h : SemanticCore.Var) : nb090AlphaDummy563 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy563 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy563 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0578 (A : SemanticCore.Class) : nb090AlphaDummy561 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy560 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy561 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0579 (h : SemanticCore.Var) : nb090AlphaDummy564 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy563 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy564 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0580 (A : SemanticCore.Class) : nb090AlphaDummy561 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy561 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy561 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0581 (h : SemanticCore.Var) : nb090AlphaDummy564 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy564 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy564 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0582 (A : SemanticCore.Class) : nb090AlphaDummy503 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy504 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy503 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0583 (A : SemanticCore.Class) : nb090AlphaDummy503 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy545 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy546 A) (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy545 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy545 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy546 A) (SemanticCore.Class.cv (nb090AlphaDummy503 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy545 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0584 (h : SemanticCore.Var) : nb090AlphaDummy505 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy506 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy505 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0585 (h : SemanticCore.Var) : nb090AlphaDummy505 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy547 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy548 h) (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy547 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy547 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy548 h) (SemanticCore.Class.cv (nb090AlphaDummy505 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy547 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0586 (A : SemanticCore.Class) : nb090AlphaDummy503 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy545 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy546 A) (SemanticCore.Class.cv (nb090AlphaDummy503 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy545 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy545 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy546 A) (SemanticCore.Class.cv (nb090AlphaDummy503 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy545 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0587 (h : SemanticCore.Var) : nb090AlphaDummy505 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy547 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy548 h) (SemanticCore.Class.cv (nb090AlphaDummy505 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy547 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy547 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy548 h) (SemanticCore.Class.cv (nb090AlphaDummy505 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy547 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0588 (A : SemanticCore.Class) : nb090AlphaDummy546 A ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0589 (h : SemanticCore.Var) : nb090AlphaDummy548 h ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0590 (A : SemanticCore.Class) : nb090AlphaDummy546 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0591 (h : SemanticCore.Var) : nb090AlphaDummy548 h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0592 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))))) Compiler.CompactSourceSyntax.synCid).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0593 (h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)))) Compiler.CompactSourceSyntax.synCid).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0594 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0595 (h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0596 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0597 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ {nb090AlphaDummy423 A} ∪ {nb090AlphaDummy424 A} ∪ (Compiler.CompactSourceSyntax.synWex (nb090AlphaDummy425 A) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy423 A)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A)))) (SemanticCore.Class.cv (nb090AlphaDummy425 A))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy425 A)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (SemanticCore.Class.cv (nb090AlphaDummy424 A))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0598 (h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0599 (h : SemanticCore.Var) : h ∈ {nb090AlphaDummy426 h} ∪ {nb090AlphaDummy427 h} ∪ (Compiler.CompactSourceSyntax.synWex (nb090AlphaDummy428 h) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy426 h)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h))) (SemanticCore.Class.cv (nb090AlphaDummy428 h))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy428 h)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (SemanticCore.Class.cv (nb090AlphaDummy427 h))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0600 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ {nb090AlphaDummy503 A} ∪ {nb090AlphaDummy504 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))) (SemanticCore.Class.cv (nb090AlphaDummy503 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0601 (h : SemanticCore.Var) : h ∈ {nb090AlphaDummy505 h} ∪ {nb090AlphaDummy506 h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (SemanticCore.Class.cv (nb090AlphaDummy505 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0602 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0603 (h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0604 (A : SemanticCore.Class) : nb090AlphaDummy425 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy425 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy424 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0605 (A : SemanticCore.Class) : nb090AlphaDummy425 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy581 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy582 A) (SemanticCore.Class.cv (nb090AlphaDummy425 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy581 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy581 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy582 A) (SemanticCore.Class.cv (nb090AlphaDummy424 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy581 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0606 (h : SemanticCore.Var) : nb090AlphaDummy428 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy428 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy427 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0607 (h : SemanticCore.Var) : nb090AlphaDummy428 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy583 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy584 h) (SemanticCore.Class.cv (nb090AlphaDummy428 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy583 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy583 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy584 h) (SemanticCore.Class.cv (nb090AlphaDummy427 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy583 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0608 (A : SemanticCore.Class) : nb090AlphaDummy425 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy581 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy582 A) (SemanticCore.Class.cv (nb090AlphaDummy425 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy581 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy581 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy582 A) (SemanticCore.Class.cv (nb090AlphaDummy425 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy581 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0609 (h : SemanticCore.Var) : nb090AlphaDummy428 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy583 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy584 h) (SemanticCore.Class.cv (nb090AlphaDummy428 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy583 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy583 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy584 h) (SemanticCore.Class.cv (nb090AlphaDummy428 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy583 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0610 (A : SemanticCore.Class) : nb090AlphaDummy582 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy582 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0611 (h : SemanticCore.Var) : nb090AlphaDummy584 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy584 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0612 (A : SemanticCore.Class) : nb090AlphaDummy589 A ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy589 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy589 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy589 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0613 (h : SemanticCore.Var) : nb090AlphaDummy591 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy591 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy591 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy591 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0614 (A : SemanticCore.Class) : nb090AlphaDummy589 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy589 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0615 (h : SemanticCore.Var) : nb090AlphaDummy591 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy591 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0616 (A : SemanticCore.Class) : nb090AlphaDummy596 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy596 A)) (SemanticCore.Class.cv (nb090AlphaDummy597 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy596 A)) (SemanticCore.Class.cv (nb090AlphaDummy597 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0617 (h : SemanticCore.Var) : nb090AlphaDummy599 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy599 h)) (SemanticCore.Class.cv (nb090AlphaDummy600 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy599 h)) (SemanticCore.Class.cv (nb090AlphaDummy600 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0618 (A : SemanticCore.Class) : nb090AlphaDummy596 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy596 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy597 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0619 (h : SemanticCore.Var) : nb090AlphaDummy599 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy599 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy600 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0620 (A : SemanticCore.Class) : nb090AlphaDummy597 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy596 A)) (SemanticCore.Class.cv (nb090AlphaDummy597 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy596 A)) (SemanticCore.Class.cv (nb090AlphaDummy597 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0621 (h : SemanticCore.Var) : nb090AlphaDummy600 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy599 h)) (SemanticCore.Class.cv (nb090AlphaDummy600 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy599 h)) (SemanticCore.Class.cv (nb090AlphaDummy600 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0622 (A : SemanticCore.Class) : nb090AlphaDummy597 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy596 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy597 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0623 (h : SemanticCore.Var) : nb090AlphaDummy600 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy599 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy600 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0624 (A : SemanticCore.Class) : nb090AlphaDummy596 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy596 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy597 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0625 (h : SemanticCore.Var) : nb090AlphaDummy599 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy599 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy600 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0626 (A : SemanticCore.Class) : nb090AlphaDummy596 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy596 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy596 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0627 (h : SemanticCore.Var) : nb090AlphaDummy599 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy599 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy599 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0628 (A : SemanticCore.Class) : nb090AlphaDummy597 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy596 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy597 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0629 (h : SemanticCore.Var) : nb090AlphaDummy600 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy599 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy600 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0630 (A : SemanticCore.Class) : nb090AlphaDummy597 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy597 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy597 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0631 (h : SemanticCore.Var) : nb090AlphaDummy600 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy600 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy600 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0632 (A : SemanticCore.Class) : nb090AlphaDummy424 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy425 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy424 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0633 (A : SemanticCore.Class) : nb090AlphaDummy424 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy581 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy582 A) (SemanticCore.Class.cv (nb090AlphaDummy425 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy581 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy581 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy582 A) (SemanticCore.Class.cv (nb090AlphaDummy424 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy581 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0634 (h : SemanticCore.Var) : nb090AlphaDummy427 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy428 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy427 h)).fv