Nominal proof certificates grouped in dependency order.

Certificates from NAR4C067C001Part006.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_371 (x y f : SemanticCore.Var) : nb067AlphaDummy068 x y f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy061 x y f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy062 x y f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_372 : nb067AlphaDummy115 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy106)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy107)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_373 (f : SemanticCore.Var) : nb067AlphaDummy116 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy109 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy110 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_374 : nb067AlphaDummy151 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy142)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy143)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_375 (f : SemanticCore.Var) : nb067AlphaDummy152 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy145 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy146 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_376 : nb067AlphaDummy193 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy184)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy185)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_377 (f : SemanticCore.Var) : nb067AlphaDummy194 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy187 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy188 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_378 : nb067AlphaDummy229 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy220)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy221)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_379 (f : SemanticCore.Var) : nb067AlphaDummy230 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy223 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy224 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_380 : nb067AlphaDummy265 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy256)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy257)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_381 (f : SemanticCore.Var) : nb067AlphaDummy266 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy259 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy260 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_382 : nb067AlphaDummy305 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy296)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy297)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_383 (f : SemanticCore.Var) : nb067AlphaDummy306 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy299 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy300 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_384 : nb067AlphaDummy349 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy340)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy341)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_385 (f : SemanticCore.Var) : nb067AlphaDummy350 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy343 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy344 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_386 : nb067AlphaDummy075 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_387 (x y f : SemanticCore.Var) : nb067AlphaDummy076 x y f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_388 : nb067AlphaDummy047 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_389 (x y : SemanticCore.Var) : nb067AlphaDummy048 x y ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_390 : nb067AlphaDummy123 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_391 (f : SemanticCore.Var) : nb067AlphaDummy124 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_392 : nb067AlphaDummy159 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_393 (f : SemanticCore.Var) : nb067AlphaDummy160 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_394 : nb067AlphaDummy201 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_395 (f : SemanticCore.Var) : nb067AlphaDummy202 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_396 : nb067AlphaDummy237 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_397 (f : SemanticCore.Var) : nb067AlphaDummy238 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_398 : nb067AlphaDummy273 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_399 (f : SemanticCore.Var) : nb067AlphaDummy274 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_400 : nb067AlphaDummy313 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_401 (f : SemanticCore.Var) : nb067AlphaDummy314 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_402 : nb067AlphaDummy357 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_403 (f : SemanticCore.Var) : nb067AlphaDummy358 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_404 : nb067AlphaDummy035 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy030) (SemanticCore.Class.cv nb067AlphaDummy031)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy030) (SemanticCore.Class.cv nb067AlphaDummy031)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_405 (x y : SemanticCore.Var) : nb067AlphaDummy036 x y ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy033 x y)) (SemanticCore.Class.cv (nb067AlphaDummy034 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy033 x y)) (SemanticCore.Class.cv (nb067AlphaDummy034 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_406 : nb067AlphaDummy063 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy058) (SemanticCore.Class.cv nb067AlphaDummy059)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy058) (SemanticCore.Class.cv nb067AlphaDummy059)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_407 (x y f : SemanticCore.Var) : nb067AlphaDummy064 x y f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy061 x y f)) (SemanticCore.Class.cv (nb067AlphaDummy062 x y f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy061 x y f)) (SemanticCore.Class.cv (nb067AlphaDummy062 x y f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_408 : nb067AlphaDummy111 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy106) (SemanticCore.Class.cv nb067AlphaDummy107)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy106) (SemanticCore.Class.cv nb067AlphaDummy107)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_409 (f : SemanticCore.Var) : nb067AlphaDummy112 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy109 f)) (SemanticCore.Class.cv (nb067AlphaDummy110 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy109 f)) (SemanticCore.Class.cv (nb067AlphaDummy110 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_410 : nb067AlphaDummy147 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy142) (SemanticCore.Class.cv nb067AlphaDummy143)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy142) (SemanticCore.Class.cv nb067AlphaDummy143)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_411 (f : SemanticCore.Var) : nb067AlphaDummy148 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy145 f)) (SemanticCore.Class.cv (nb067AlphaDummy146 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy145 f)) (SemanticCore.Class.cv (nb067AlphaDummy146 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_412 : nb067AlphaDummy189 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy184) (SemanticCore.Class.cv nb067AlphaDummy185)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy184) (SemanticCore.Class.cv nb067AlphaDummy185)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_413 (f : SemanticCore.Var) : nb067AlphaDummy190 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy187 f)) (SemanticCore.Class.cv (nb067AlphaDummy188 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy187 f)) (SemanticCore.Class.cv (nb067AlphaDummy188 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_414 : nb067AlphaDummy225 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy220) (SemanticCore.Class.cv nb067AlphaDummy221)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy220) (SemanticCore.Class.cv nb067AlphaDummy221)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_415 (f : SemanticCore.Var) : nb067AlphaDummy226 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy223 f)) (SemanticCore.Class.cv (nb067AlphaDummy224 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy223 f)) (SemanticCore.Class.cv (nb067AlphaDummy224 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_416 : nb067AlphaDummy261 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy256) (SemanticCore.Class.cv nb067AlphaDummy257)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy256) (SemanticCore.Class.cv nb067AlphaDummy257)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_417 (f : SemanticCore.Var) : nb067AlphaDummy262 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy259 f)) (SemanticCore.Class.cv (nb067AlphaDummy260 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy259 f)) (SemanticCore.Class.cv (nb067AlphaDummy260 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_418 : nb067AlphaDummy301 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy296) (SemanticCore.Class.cv nb067AlphaDummy297)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy296) (SemanticCore.Class.cv nb067AlphaDummy297)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_419 (f : SemanticCore.Var) : nb067AlphaDummy302 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy299 f)) (SemanticCore.Class.cv (nb067AlphaDummy300 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy299 f)) (SemanticCore.Class.cv (nb067AlphaDummy300 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_420 : nb067AlphaDummy345 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_421 (f : SemanticCore.Var) : nb067AlphaDummy346 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_422 : nb067AlphaDummy079 ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb067AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb067AlphaDummy000))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb067AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb067AlphaDummy000))) Compiler.CompactSourceSyntax.synCid).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_423 (f : SemanticCore.Var) : nb067AlphaDummy080 f ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_424 : nb067AlphaDummy317 ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy001)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy001)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_425 (x f : SemanticCore.Var) : nb067AlphaDummy318 x f ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv x)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_426 : nb067AlphaDummy007 ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy003).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_427 : nb067AlphaDummy008 ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy003).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_distinct_428 : nb067AlphaDummy007 ≠ nb067AlphaDummy008

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_429 (x y f : SemanticCore.Var) : nb067AlphaDummy009 x y f ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_430 (x y f : SemanticCore.Var) : nb067AlphaDummy010 x y f ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_distinct_431 (x y f : SemanticCore.Var) : nb067AlphaDummy009 x y f ≠ nb067AlphaDummy010 x y f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_432 : nb067AlphaDummy077 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_433 (x y f : SemanticCore.Var) : nb067AlphaDummy078 x y f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_434 : nb067AlphaDummy049 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_435 (x y : SemanticCore.Var) : nb067AlphaDummy050 x y ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_436 : nb067AlphaDummy125 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_437 (f : SemanticCore.Var) : nb067AlphaDummy126 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_438 : nb067AlphaDummy161 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_439 (f : SemanticCore.Var) : nb067AlphaDummy162 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_440 : nb067AlphaDummy203 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_441 (f : SemanticCore.Var) : nb067AlphaDummy204 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_442 : nb067AlphaDummy239 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_443 (f : SemanticCore.Var) : nb067AlphaDummy240 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_444 : nb067AlphaDummy275 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_445 (f : SemanticCore.Var) : nb067AlphaDummy276 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_446 : nb067AlphaDummy315 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_447 (f : SemanticCore.Var) : nb067AlphaDummy316 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_448 : nb067AlphaDummy359 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_449 (f : SemanticCore.Var) : nb067AlphaDummy360 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_450 : nb067AlphaDummy319 ∉ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb067AlphaDummy000)).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_451 (x f : SemanticCore.Var) : nb067AlphaDummy320 x f ∉ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)).fv ∪ (SemanticCore.Class.cv x).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_452 : nb067AlphaDummy003 ∉ {nb067AlphaDummy001} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ {nb067AlphaDummy002} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (SemanticCore.Class.cab nb067AlphaDummy000 (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Class.cv nb067AlphaDummy001))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_453 : nb067AlphaDummy005 ∉ {nb067AlphaDummy001} ∪ {nb067AlphaDummy002} ∪ {nb067AlphaDummy003} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy001) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy002) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy003) (SemanticCore.Class.cab nb067AlphaDummy000 (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Class.cv nb067AlphaDummy001))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_454 : nb067AlphaDummy089 ∉ {nb067AlphaDummy083} ∪ {nb067AlphaDummy084} ∪ (Compiler.CompactSourceSyntax.synWex nb067AlphaDummy085 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy083) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy085)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy084)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_455 (f : SemanticCore.Var) : nb067AlphaDummy090 f ∉ {nb067AlphaDummy086 f} ∪ {nb067AlphaDummy087 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb067AlphaDummy088 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb067AlphaDummy088 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb067AlphaDummy087 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_456 : nb067AlphaDummy167 ∉ {nb067AlphaDummy163} ∪ {nb067AlphaDummy164} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy163)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_457 (f : SemanticCore.Var) : nb067AlphaDummy168 f ∉ {nb067AlphaDummy165 f} ∪ {nb067AlphaDummy166 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb067AlphaDummy165 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_458 (x y f : SemanticCore.Var) : nb067AlphaDummy004 x y f ∉ {x} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ {y} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv y) (SemanticCore.Class.cv x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_459 (x y f : SemanticCore.Var) : nb067AlphaDummy006 x y f ∉ {x} ∪ {y} ∪ {nb067AlphaDummy004 x y f} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)) (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv y) (SemanticCore.Class.cv x))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_460 : nb067AlphaDummy000 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_461 : nb067AlphaDummy001 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_fresh_462 : nb067AlphaDummy002 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_distinct_463 : nb067AlphaDummy000 ≠ nb067AlphaDummy001

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_distinct_464 : nb067AlphaDummy000 ≠ nb067AlphaDummy002

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_distinct_465 : nb067AlphaDummy001 ≠ nb067AlphaDummy002

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0000 : nb067AlphaDummy001 ∈ {nb067AlphaDummy001} ∪ {nb067AlphaDummy002} ∪ {nb067AlphaDummy003} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy001) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy002) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy003) (SemanticCore.Class.cab nb067AlphaDummy000 (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Class.cv nb067AlphaDummy001))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0001 (x y f : SemanticCore.Var) : x ∈ {x} ∪ {y} ∪ {nb067AlphaDummy004 x y f} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)) (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv y) (SemanticCore.Class.cv x))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0002 : nb067AlphaDummy002 ∈ {nb067AlphaDummy001} ∪ {nb067AlphaDummy002} ∪ {nb067AlphaDummy003} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy001) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy002) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy003) (SemanticCore.Class.cab nb067AlphaDummy000 (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Class.cv nb067AlphaDummy001))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0003 (x y f : SemanticCore.Var) : y ∈ {x} ∪ {y} ∪ {nb067AlphaDummy004 x y f} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)) (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv y) (SemanticCore.Class.cv x))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0004 : nb067AlphaDummy003 ∈ {nb067AlphaDummy001} ∪ {nb067AlphaDummy002} ∪ {nb067AlphaDummy003} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy001) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy002) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy003) (SemanticCore.Class.cab nb067AlphaDummy000 (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Class.cv nb067AlphaDummy001))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0005 (x y f : SemanticCore.Var) : nb067AlphaDummy004 x y f ∈ {x} ∪ {y} ∪ {nb067AlphaDummy004 x y f} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)) (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv y) (SemanticCore.Class.cv x))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0006 : nb067AlphaDummy001 ∈ {nb067AlphaDummy001} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ {nb067AlphaDummy002} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (SemanticCore.Class.cab nb067AlphaDummy000 (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Class.cv nb067AlphaDummy001))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0007 (x y f : SemanticCore.Var) : x ∈ {x} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ {y} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv y) (SemanticCore.Class.cv x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0008 : nb067AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy003).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0009 : nb067AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy007 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy007 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (SemanticCore.Class.cv nb067AlphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0010 (x y f : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0011 (x y f : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy009 x y f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy009 x y f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f) (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0012 : nb067AlphaDummy001 ∈ (SemanticCore.Class.cab nb067AlphaDummy007 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy007 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0013 (x y f : SemanticCore.Var) : x ∈ (SemanticCore.Class.cab (nb067AlphaDummy009 x y f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f)))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy009 x y f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0014 : nb067AlphaDummy001 ∈ (SemanticCore.Class.cv nb067AlphaDummy001).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0015 : nb067AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy015 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy016 (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy015) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy015 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy016 (SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy015) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0016 (x y : SemanticCore.Var) : x ∈ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0017 (x y : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy017 x y) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy018 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy017 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy017 x y) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy018 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy017 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0018 : nb067AlphaDummy001 ∈ (SemanticCore.Class.cab nb067AlphaDummy015 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy016 (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy015) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy015 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy016 (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy015) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0019 (x y : SemanticCore.Var) : x ∈ (SemanticCore.Class.cab (nb067AlphaDummy017 x y) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy018 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy017 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y)))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy017 x y) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy018 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy017 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0020 : nb067AlphaDummy016 ∈ (SemanticCore.Class.cv nb067AlphaDummy016).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0021 (x y : SemanticCore.Var) : nb067AlphaDummy018 x y ∈ (SemanticCore.Class.cv (nb067AlphaDummy018 x y)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0023 (x y : SemanticCore.Var) : nb067AlphaDummy025 x y ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy025 x y)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy025 x y)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy025 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0024 : nb067AlphaDummy023 ∈ (SemanticCore.Class.cv nb067AlphaDummy023).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0025 (x y : SemanticCore.Var) : nb067AlphaDummy025 x y ∈ (SemanticCore.Class.cv (nb067AlphaDummy025 x y)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0026 : nb067AlphaDummy030 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy030) (SemanticCore.Class.cv nb067AlphaDummy031)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy030) (SemanticCore.Class.cv nb067AlphaDummy031)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0027 (x y : SemanticCore.Var) : nb067AlphaDummy033 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy033 x y)) (SemanticCore.Class.cv (nb067AlphaDummy034 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy033 x y)) (SemanticCore.Class.cv (nb067AlphaDummy034 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0028 : nb067AlphaDummy030 ∈ (SemanticCore.Class.cv nb067AlphaDummy030).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy031).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0029 (x y : SemanticCore.Var) : nb067AlphaDummy033 x y ∈ (SemanticCore.Class.cv (nb067AlphaDummy033 x y)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy034 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0030 : nb067AlphaDummy031 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy030) (SemanticCore.Class.cv nb067AlphaDummy031)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy030) (SemanticCore.Class.cv nb067AlphaDummy031)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0031 (x y : SemanticCore.Var) : nb067AlphaDummy034 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy033 x y)) (SemanticCore.Class.cv (nb067AlphaDummy034 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy033 x y)) (SemanticCore.Class.cv (nb067AlphaDummy034 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0032 : nb067AlphaDummy031 ∈ (SemanticCore.Class.cv nb067AlphaDummy030).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy031).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0033 (x y : SemanticCore.Var) : nb067AlphaDummy034 x y ∈ (SemanticCore.Class.cv (nb067AlphaDummy033 x y)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy034 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0034 : nb067AlphaDummy030 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy030)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy031)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0035 (x y : SemanticCore.Var) : nb067AlphaDummy033 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy033 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy034 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0036 : nb067AlphaDummy030 ∈ (SemanticCore.Class.cv nb067AlphaDummy030).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy030).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0037 (x y : SemanticCore.Var) : nb067AlphaDummy033 x y ∈ (SemanticCore.Class.cv (nb067AlphaDummy033 x y)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy033 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0038 : nb067AlphaDummy031 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy030)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy031)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0039 (x y : SemanticCore.Var) : nb067AlphaDummy034 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy033 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy034 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0040 : nb067AlphaDummy031 ∈ (SemanticCore.Class.cv nb067AlphaDummy031).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy031).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0041 (x y : SemanticCore.Var) : nb067AlphaDummy034 x y ∈ (SemanticCore.Class.cv (nb067AlphaDummy034 x y)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy034 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0042 : nb067AlphaDummy002 ∈ {nb067AlphaDummy001} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ {nb067AlphaDummy002} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (SemanticCore.Class.cab nb067AlphaDummy000 (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Class.cv nb067AlphaDummy001))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0043 (x y f : SemanticCore.Var) : y ∈ {x} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ {y} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv y) (SemanticCore.Class.cv x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0044 : nb067AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy003).fv

Certificates from NAR4C067C001Part007.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0045 : nb067AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy007 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy007 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (SemanticCore.Class.cv nb067AlphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0046 (x y f : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0047 (x y f : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy009 x y f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy009 x y f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f) (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0048 : nb067AlphaDummy002 ∈ (SemanticCore.Class.cab nb067AlphaDummy007 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy007 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0049 (x y f : SemanticCore.Var) : y ∈ (SemanticCore.Class.cab (nb067AlphaDummy009 x y f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f)))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy009 x y f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0050 : nb067AlphaDummy002 ∈ (SemanticCore.Class.cv nb067AlphaDummy001).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0051 : nb067AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy015 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy016 (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy015) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy015 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy016 (SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy015) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0052 (x y : SemanticCore.Var) : y ∈ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0053 (x y : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy017 x y) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy018 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy017 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy017 x y) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy018 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy017 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0054 : nb067AlphaDummy002 ∈ (SemanticCore.Class.cab nb067AlphaDummy015 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy016 (SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy015) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy015 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy016 (SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy015) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0055 (x y : SemanticCore.Var) : y ∈ (SemanticCore.Class.cab (nb067AlphaDummy017 x y) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy018 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy017 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy017 x y) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy018 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy017 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0057 (x y : SemanticCore.Var) : nb067AlphaDummy018 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0058 : nb067AlphaDummy016 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy016)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0059 (x y : SemanticCore.Var) : nb067AlphaDummy018 x y ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy018 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0060 : nb067AlphaDummy008 ∈ (SemanticCore.Class.cv nb067AlphaDummy008).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0061 (x y f : SemanticCore.Var) : nb067AlphaDummy010 x y f ∈ (SemanticCore.Class.cv (nb067AlphaDummy010 x y f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0063 (x y f : SemanticCore.Var) : nb067AlphaDummy053 x y f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy053 x y f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy053 x y f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy053 x y f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0064 : nb067AlphaDummy051 ∈ (SemanticCore.Class.cv nb067AlphaDummy051).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0065 (x y f : SemanticCore.Var) : nb067AlphaDummy053 x y f ∈ (SemanticCore.Class.cv (nb067AlphaDummy053 x y f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0066 : nb067AlphaDummy058 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy058) (SemanticCore.Class.cv nb067AlphaDummy059)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy058) (SemanticCore.Class.cv nb067AlphaDummy059)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0067 (x y f : SemanticCore.Var) : nb067AlphaDummy061 x y f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy061 x y f)) (SemanticCore.Class.cv (nb067AlphaDummy062 x y f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy061 x y f)) (SemanticCore.Class.cv (nb067AlphaDummy062 x y f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0068 : nb067AlphaDummy058 ∈ (SemanticCore.Class.cv nb067AlphaDummy058).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy059).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0069 (x y f : SemanticCore.Var) : nb067AlphaDummy061 x y f ∈ (SemanticCore.Class.cv (nb067AlphaDummy061 x y f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy062 x y f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0070 : nb067AlphaDummy059 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy058) (SemanticCore.Class.cv nb067AlphaDummy059)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy058) (SemanticCore.Class.cv nb067AlphaDummy059)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0071 (x y f : SemanticCore.Var) : nb067AlphaDummy062 x y f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy061 x y f)) (SemanticCore.Class.cv (nb067AlphaDummy062 x y f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy061 x y f)) (SemanticCore.Class.cv (nb067AlphaDummy062 x y f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0072 : nb067AlphaDummy059 ∈ (SemanticCore.Class.cv nb067AlphaDummy058).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy059).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0073 (x y f : SemanticCore.Var) : nb067AlphaDummy062 x y f ∈ (SemanticCore.Class.cv (nb067AlphaDummy061 x y f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy062 x y f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0074 : nb067AlphaDummy058 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy058)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy059)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0075 (x y f : SemanticCore.Var) : nb067AlphaDummy061 x y f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy061 x y f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy062 x y f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0076 : nb067AlphaDummy058 ∈ (SemanticCore.Class.cv nb067AlphaDummy058).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy058).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0077 (x y f : SemanticCore.Var) : nb067AlphaDummy061 x y f ∈ (SemanticCore.Class.cv (nb067AlphaDummy061 x y f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy061 x y f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0078 : nb067AlphaDummy059 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy058)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy059)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0079 (x y f : SemanticCore.Var) : nb067AlphaDummy062 x y f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy061 x y f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy062 x y f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0080 : nb067AlphaDummy059 ∈ (SemanticCore.Class.cv nb067AlphaDummy059).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy059).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0081 (x y f : SemanticCore.Var) : nb067AlphaDummy062 x y f ∈ (SemanticCore.Class.cv (nb067AlphaDummy062 x y f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy062 x y f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0082 : nb067AlphaDummy003 ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy003).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0083 : nb067AlphaDummy003 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy007 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy007 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (SemanticCore.Class.cv nb067AlphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0084 (x y f : SemanticCore.Var) : nb067AlphaDummy004 x y f ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0085 (x y f : SemanticCore.Var) : nb067AlphaDummy004 x y f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy009 x y f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy009 x y f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f) (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0086 : nb067AlphaDummy003 ∈ (SemanticCore.Class.cab nb067AlphaDummy007 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (SemanticCore.Class.cv nb067AlphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy007 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy008 (SemanticCore.Class.cv nb067AlphaDummy003) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy007) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0087 (x y f : SemanticCore.Var) : nb067AlphaDummy004 x y f ∈ (SemanticCore.Class.cab (nb067AlphaDummy009 x y f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f) (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy009 x y f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy010 x y f) (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy009 x y f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0089 (x y f : SemanticCore.Var) : nb067AlphaDummy010 x y f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0090 : nb067AlphaDummy008 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy008)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0091 (x y f : SemanticCore.Var) : nb067AlphaDummy010 x y f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy010 x y f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0092 : nb067AlphaDummy083 ∈ {nb067AlphaDummy083} ∪ {nb067AlphaDummy084} ∪ (Compiler.CompactSourceSyntax.synWex nb067AlphaDummy085 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy083) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy085)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy084)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0093 (f : SemanticCore.Var) : nb067AlphaDummy086 f ∈ {nb067AlphaDummy086 f} ∪ {nb067AlphaDummy087 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb067AlphaDummy088 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb067AlphaDummy088 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb067AlphaDummy087 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0094 : nb067AlphaDummy084 ∈ {nb067AlphaDummy083} ∪ {nb067AlphaDummy084} ∪ (Compiler.CompactSourceSyntax.synWex nb067AlphaDummy085 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy083) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy085)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy084)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0095 (f : SemanticCore.Var) : nb067AlphaDummy087 f ∈ {nb067AlphaDummy086 f} ∪ {nb067AlphaDummy087 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb067AlphaDummy088 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb067AlphaDummy088 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb067AlphaDummy087 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0096 : nb067AlphaDummy083 ∈ (SemanticCore.Class.cv nb067AlphaDummy083).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy084).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0097 : nb067AlphaDummy083 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy091 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy092 (SemanticCore.Class.cv nb067AlphaDummy083) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy091) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy091 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy092 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy091) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0098 (f : SemanticCore.Var) : nb067AlphaDummy086 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy086 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy087 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0099 (f : SemanticCore.Var) : nb067AlphaDummy086 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy093 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy094 f) (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy093 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy094 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0100 : nb067AlphaDummy083 ∈ (SemanticCore.Class.cab nb067AlphaDummy091 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy092 (SemanticCore.Class.cv nb067AlphaDummy083) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy091) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy091 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy092 (SemanticCore.Class.cv nb067AlphaDummy083) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy091) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0101 (f : SemanticCore.Var) : nb067AlphaDummy086 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy093 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy094 f) (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f)))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy093 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy094 f) (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0102 : nb067AlphaDummy092 ∈ (SemanticCore.Class.cv nb067AlphaDummy092).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0103 (f : SemanticCore.Var) : nb067AlphaDummy094 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy094 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0105 (f : SemanticCore.Var) : nb067AlphaDummy101 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy101 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy101 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy101 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0106 : nb067AlphaDummy099 ∈ (SemanticCore.Class.cv nb067AlphaDummy099).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0107 (f : SemanticCore.Var) : nb067AlphaDummy101 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy101 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0108 : nb067AlphaDummy106 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy106) (SemanticCore.Class.cv nb067AlphaDummy107)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy106) (SemanticCore.Class.cv nb067AlphaDummy107)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0109 (f : SemanticCore.Var) : nb067AlphaDummy109 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy109 f)) (SemanticCore.Class.cv (nb067AlphaDummy110 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy109 f)) (SemanticCore.Class.cv (nb067AlphaDummy110 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0110 : nb067AlphaDummy106 ∈ (SemanticCore.Class.cv nb067AlphaDummy106).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy107).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0111 (f : SemanticCore.Var) : nb067AlphaDummy109 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy109 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy110 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0112 : nb067AlphaDummy107 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy106) (SemanticCore.Class.cv nb067AlphaDummy107)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy106) (SemanticCore.Class.cv nb067AlphaDummy107)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0113 (f : SemanticCore.Var) : nb067AlphaDummy110 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy109 f)) (SemanticCore.Class.cv (nb067AlphaDummy110 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy109 f)) (SemanticCore.Class.cv (nb067AlphaDummy110 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0114 : nb067AlphaDummy107 ∈ (SemanticCore.Class.cv nb067AlphaDummy106).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy107).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0115 (f : SemanticCore.Var) : nb067AlphaDummy110 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy109 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy110 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0116 : nb067AlphaDummy106 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy106)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy107)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0117 (f : SemanticCore.Var) : nb067AlphaDummy109 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy109 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy110 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0118 : nb067AlphaDummy106 ∈ (SemanticCore.Class.cv nb067AlphaDummy106).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy106).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0119 (f : SemanticCore.Var) : nb067AlphaDummy109 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy109 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy109 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0120 : nb067AlphaDummy107 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy106)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy107)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0121 (f : SemanticCore.Var) : nb067AlphaDummy110 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy109 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy110 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0122 : nb067AlphaDummy107 ∈ (SemanticCore.Class.cv nb067AlphaDummy107).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy107).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0123 (f : SemanticCore.Var) : nb067AlphaDummy110 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy110 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy110 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0124 : nb067AlphaDummy084 ∈ (SemanticCore.Class.cv nb067AlphaDummy083).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy084).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0125 : nb067AlphaDummy084 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy091 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy092 (SemanticCore.Class.cv nb067AlphaDummy083) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy091) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy091 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy092 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy091) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0126 (f : SemanticCore.Var) : nb067AlphaDummy087 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy086 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy087 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0127 (f : SemanticCore.Var) : nb067AlphaDummy087 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy093 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy094 f) (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy093 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy094 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0128 : nb067AlphaDummy084 ∈ (SemanticCore.Class.cab nb067AlphaDummy091 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy092 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy091) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy091 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy092 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy091) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0129 (f : SemanticCore.Var) : nb067AlphaDummy087 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy093 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy094 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy093 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy094 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0131 (f : SemanticCore.Var) : nb067AlphaDummy094 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0132 : nb067AlphaDummy092 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0133 (f : SemanticCore.Var) : nb067AlphaDummy094 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0134 : nb067AlphaDummy083 ∈ (SemanticCore.Class.cv nb067AlphaDummy083).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy085).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0135 : nb067AlphaDummy083 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy127 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy128 (SemanticCore.Class.cv nb067AlphaDummy083) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy127) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy127 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy128 (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy127) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0136 (f : SemanticCore.Var) : nb067AlphaDummy086 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy086 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy088 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0137 (f : SemanticCore.Var) : nb067AlphaDummy086 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy129 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy130 f) (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy129 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy130 f) (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0138 : nb067AlphaDummy083 ∈ (SemanticCore.Class.cab nb067AlphaDummy127 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy128 (SemanticCore.Class.cv nb067AlphaDummy083) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy127) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy127 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy128 (SemanticCore.Class.cv nb067AlphaDummy083) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy127) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0139 (f : SemanticCore.Var) : nb067AlphaDummy086 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy129 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy130 f) (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f)))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy129 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy130 f) (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0140 : nb067AlphaDummy128 ∈ (SemanticCore.Class.cv nb067AlphaDummy128).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0141 (f : SemanticCore.Var) : nb067AlphaDummy130 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy130 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0143 (f : SemanticCore.Var) : nb067AlphaDummy137 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy137 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy137 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy137 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0144 : nb067AlphaDummy135 ∈ (SemanticCore.Class.cv nb067AlphaDummy135).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0145 (f : SemanticCore.Var) : nb067AlphaDummy137 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy137 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0146 : nb067AlphaDummy142 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy142) (SemanticCore.Class.cv nb067AlphaDummy143)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy142) (SemanticCore.Class.cv nb067AlphaDummy143)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0147 (f : SemanticCore.Var) : nb067AlphaDummy145 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy145 f)) (SemanticCore.Class.cv (nb067AlphaDummy146 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy145 f)) (SemanticCore.Class.cv (nb067AlphaDummy146 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0148 : nb067AlphaDummy142 ∈ (SemanticCore.Class.cv nb067AlphaDummy142).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy143).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0149 (f : SemanticCore.Var) : nb067AlphaDummy145 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy145 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy146 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0150 : nb067AlphaDummy143 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy142) (SemanticCore.Class.cv nb067AlphaDummy143)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy142) (SemanticCore.Class.cv nb067AlphaDummy143)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0151 (f : SemanticCore.Var) : nb067AlphaDummy146 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy145 f)) (SemanticCore.Class.cv (nb067AlphaDummy146 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy145 f)) (SemanticCore.Class.cv (nb067AlphaDummy146 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0152 : nb067AlphaDummy143 ∈ (SemanticCore.Class.cv nb067AlphaDummy142).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy143).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0153 (f : SemanticCore.Var) : nb067AlphaDummy146 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy145 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy146 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0154 : nb067AlphaDummy142 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy142)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy143)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0155 (f : SemanticCore.Var) : nb067AlphaDummy145 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy145 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy146 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0156 : nb067AlphaDummy142 ∈ (SemanticCore.Class.cv nb067AlphaDummy142).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy142).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0157 (f : SemanticCore.Var) : nb067AlphaDummy145 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy145 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy145 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0158 : nb067AlphaDummy143 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy142)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy143)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0159 (f : SemanticCore.Var) : nb067AlphaDummy146 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy145 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy146 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0160 : nb067AlphaDummy143 ∈ (SemanticCore.Class.cv nb067AlphaDummy143).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy143).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0161 (f : SemanticCore.Var) : nb067AlphaDummy146 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy146 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy146 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0162 : nb067AlphaDummy085 ∈ (SemanticCore.Class.cv nb067AlphaDummy083).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy085).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0163 : nb067AlphaDummy085 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy127 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy128 (SemanticCore.Class.cv nb067AlphaDummy083) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy127) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy127 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy128 (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy127) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0164 (f : SemanticCore.Var) : nb067AlphaDummy088 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy086 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy088 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0165 (f : SemanticCore.Var) : nb067AlphaDummy088 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy129 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy130 f) (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy129 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy130 f) (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0166 : nb067AlphaDummy085 ∈ (SemanticCore.Class.cab nb067AlphaDummy127 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy128 (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy127) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy127 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy128 (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy127) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0167 (f : SemanticCore.Var) : nb067AlphaDummy088 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy129 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy130 f) (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy129 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy130 f) (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0169 (f : SemanticCore.Var) : nb067AlphaDummy130 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0170 : nb067AlphaDummy128 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0171 (f : SemanticCore.Var) : nb067AlphaDummy130 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0172 : nb067AlphaDummy163 ∈ {nb067AlphaDummy163} ∪ {nb067AlphaDummy164} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy163)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0173 (f : SemanticCore.Var) : nb067AlphaDummy165 f ∈ {nb067AlphaDummy165 f} ∪ {nb067AlphaDummy166 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb067AlphaDummy165 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0174 : nb067AlphaDummy164 ∈ {nb067AlphaDummy163} ∪ {nb067AlphaDummy164} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy163)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0175 (f : SemanticCore.Var) : nb067AlphaDummy166 f ∈ {nb067AlphaDummy165 f} ∪ {nb067AlphaDummy166 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb067AlphaDummy165 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0176 : nb067AlphaDummy163 ∈ (SemanticCore.Class.cv nb067AlphaDummy163).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy164).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0177 : nb067AlphaDummy163 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy169 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy170 (SemanticCore.Class.cv nb067AlphaDummy163) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy169) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy169 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy170 (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy169) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

Certificates from NAR4C067C001Part008.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0178 (f : SemanticCore.Var) : nb067AlphaDummy165 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy165 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy166 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0179 (f : SemanticCore.Var) : nb067AlphaDummy165 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy172 f) (SemanticCore.Class.cv (nb067AlphaDummy165 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy172 f) (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0180 : nb067AlphaDummy163 ∈ (SemanticCore.Class.cab nb067AlphaDummy169 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy170 (SemanticCore.Class.cv nb067AlphaDummy163) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy169) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy169 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy170 (SemanticCore.Class.cv nb067AlphaDummy163) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy169) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0181 (f : SemanticCore.Var) : nb067AlphaDummy165 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy172 f) (SemanticCore.Class.cv (nb067AlphaDummy165 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f)))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy172 f) (SemanticCore.Class.cv (nb067AlphaDummy165 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0182 : nb067AlphaDummy170 ∈ (SemanticCore.Class.cv nb067AlphaDummy170).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0183 (f : SemanticCore.Var) : nb067AlphaDummy172 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy172 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0185 (f : SemanticCore.Var) : nb067AlphaDummy179 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy179 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy179 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy179 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0186 : nb067AlphaDummy177 ∈ (SemanticCore.Class.cv nb067AlphaDummy177).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0187 (f : SemanticCore.Var) : nb067AlphaDummy179 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy179 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0188 : nb067AlphaDummy184 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy184) (SemanticCore.Class.cv nb067AlphaDummy185)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy184) (SemanticCore.Class.cv nb067AlphaDummy185)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0189 (f : SemanticCore.Var) : nb067AlphaDummy187 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy187 f)) (SemanticCore.Class.cv (nb067AlphaDummy188 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy187 f)) (SemanticCore.Class.cv (nb067AlphaDummy188 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0190 : nb067AlphaDummy184 ∈ (SemanticCore.Class.cv nb067AlphaDummy184).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy185).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0191 (f : SemanticCore.Var) : nb067AlphaDummy187 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy187 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy188 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0192 : nb067AlphaDummy185 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy184) (SemanticCore.Class.cv nb067AlphaDummy185)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy184) (SemanticCore.Class.cv nb067AlphaDummy185)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0193 (f : SemanticCore.Var) : nb067AlphaDummy188 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy187 f)) (SemanticCore.Class.cv (nb067AlphaDummy188 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy187 f)) (SemanticCore.Class.cv (nb067AlphaDummy188 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0194 : nb067AlphaDummy185 ∈ (SemanticCore.Class.cv nb067AlphaDummy184).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy185).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0195 (f : SemanticCore.Var) : nb067AlphaDummy188 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy187 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy188 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0196 : nb067AlphaDummy184 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy184)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy185)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0197 (f : SemanticCore.Var) : nb067AlphaDummy187 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy187 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy188 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0198 : nb067AlphaDummy184 ∈ (SemanticCore.Class.cv nb067AlphaDummy184).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy184).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0199 (f : SemanticCore.Var) : nb067AlphaDummy187 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy187 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy187 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0200 : nb067AlphaDummy185 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy184)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy185)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0201 (f : SemanticCore.Var) : nb067AlphaDummy188 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy187 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy188 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0202 : nb067AlphaDummy185 ∈ (SemanticCore.Class.cv nb067AlphaDummy185).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy185).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0203 (f : SemanticCore.Var) : nb067AlphaDummy188 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy188 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy188 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0204 : nb067AlphaDummy164 ∈ (SemanticCore.Class.cv nb067AlphaDummy163).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy164).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0205 : nb067AlphaDummy164 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy169 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy170 (SemanticCore.Class.cv nb067AlphaDummy163) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy169) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy169 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy170 (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy169) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0206 (f : SemanticCore.Var) : nb067AlphaDummy166 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy165 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy166 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0207 (f : SemanticCore.Var) : nb067AlphaDummy166 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy172 f) (SemanticCore.Class.cv (nb067AlphaDummy165 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy172 f) (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0208 : nb067AlphaDummy164 ∈ (SemanticCore.Class.cab nb067AlphaDummy169 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy170 (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy169) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy169 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy170 (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy169) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0209 (f : SemanticCore.Var) : nb067AlphaDummy166 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy172 f) (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy172 f) (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0211 (f : SemanticCore.Var) : nb067AlphaDummy172 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0212 : nb067AlphaDummy170 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0213 (f : SemanticCore.Var) : nb067AlphaDummy172 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0214 : nb067AlphaDummy164 ∈ (SemanticCore.Class.cv nb067AlphaDummy164).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy163).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0215 : nb067AlphaDummy164 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy205 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy206 (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy205) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy205 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy206 (SemanticCore.Class.cv nb067AlphaDummy163) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy205) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0216 (f : SemanticCore.Var) : nb067AlphaDummy166 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy166 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy165 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0217 (f : SemanticCore.Var) : nb067AlphaDummy166 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy207 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy208 f) (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy207 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy207 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy208 f) (SemanticCore.Class.cv (nb067AlphaDummy165 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy207 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0218 : nb067AlphaDummy164 ∈ (SemanticCore.Class.cab nb067AlphaDummy205 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy206 (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy205) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy205 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy206 (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy205) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0219 (f : SemanticCore.Var) : nb067AlphaDummy166 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy207 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy208 f) (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy207 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f)))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy207 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy208 f) (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy207 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0220 : nb067AlphaDummy206 ∈ (SemanticCore.Class.cv nb067AlphaDummy206).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0221 (f : SemanticCore.Var) : nb067AlphaDummy208 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy208 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0223 (f : SemanticCore.Var) : nb067AlphaDummy215 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy215 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy215 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy215 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0224 : nb067AlphaDummy213 ∈ (SemanticCore.Class.cv nb067AlphaDummy213).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0225 (f : SemanticCore.Var) : nb067AlphaDummy215 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy215 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0226 : nb067AlphaDummy220 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy220) (SemanticCore.Class.cv nb067AlphaDummy221)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy220) (SemanticCore.Class.cv nb067AlphaDummy221)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0227 (f : SemanticCore.Var) : nb067AlphaDummy223 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy223 f)) (SemanticCore.Class.cv (nb067AlphaDummy224 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy223 f)) (SemanticCore.Class.cv (nb067AlphaDummy224 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0228 : nb067AlphaDummy220 ∈ (SemanticCore.Class.cv nb067AlphaDummy220).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy221).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0229 (f : SemanticCore.Var) : nb067AlphaDummy223 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy223 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy224 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0230 : nb067AlphaDummy221 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy220) (SemanticCore.Class.cv nb067AlphaDummy221)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy220) (SemanticCore.Class.cv nb067AlphaDummy221)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0231 (f : SemanticCore.Var) : nb067AlphaDummy224 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy223 f)) (SemanticCore.Class.cv (nb067AlphaDummy224 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy223 f)) (SemanticCore.Class.cv (nb067AlphaDummy224 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0232 : nb067AlphaDummy221 ∈ (SemanticCore.Class.cv nb067AlphaDummy220).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy221).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0233 (f : SemanticCore.Var) : nb067AlphaDummy224 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy223 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy224 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0234 : nb067AlphaDummy220 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy220)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy221)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0235 (f : SemanticCore.Var) : nb067AlphaDummy223 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy223 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy224 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0236 : nb067AlphaDummy220 ∈ (SemanticCore.Class.cv nb067AlphaDummy220).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy220).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0237 (f : SemanticCore.Var) : nb067AlphaDummy223 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy223 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy223 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0238 : nb067AlphaDummy221 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy220)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy221)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0239 (f : SemanticCore.Var) : nb067AlphaDummy224 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy223 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy224 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0240 : nb067AlphaDummy221 ∈ (SemanticCore.Class.cv nb067AlphaDummy221).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy221).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0241 (f : SemanticCore.Var) : nb067AlphaDummy224 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy224 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy224 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0242 : nb067AlphaDummy163 ∈ (SemanticCore.Class.cv nb067AlphaDummy164).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy163).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0243 : nb067AlphaDummy163 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy205 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy206 (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy205) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy205 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy206 (SemanticCore.Class.cv nb067AlphaDummy163) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy205) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0244 (f : SemanticCore.Var) : nb067AlphaDummy165 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy166 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy165 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0245 (f : SemanticCore.Var) : nb067AlphaDummy165 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy207 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy208 f) (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy207 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy207 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy208 f) (SemanticCore.Class.cv (nb067AlphaDummy165 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy207 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0246 : nb067AlphaDummy163 ∈ (SemanticCore.Class.cab nb067AlphaDummy205 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy206 (SemanticCore.Class.cv nb067AlphaDummy163) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy205) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy205 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy206 (SemanticCore.Class.cv nb067AlphaDummy163) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy205) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0247 (f : SemanticCore.Var) : nb067AlphaDummy165 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy207 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy208 f) (SemanticCore.Class.cv (nb067AlphaDummy165 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy207 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy207 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy208 f) (SemanticCore.Class.cv (nb067AlphaDummy165 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy207 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0249 (f : SemanticCore.Var) : nb067AlphaDummy208 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0250 : nb067AlphaDummy206 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0251 (f : SemanticCore.Var) : nb067AlphaDummy208 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0254 : nb067AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb067AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb067AlphaDummy000))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0256 : nb067AlphaDummy000 ∈ (SemanticCore.Class.cv nb067AlphaDummy000).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb067AlphaDummy000)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0257 : nb067AlphaDummy000 ∈ {nb067AlphaDummy083} ∪ {nb067AlphaDummy084} ∪ (Compiler.CompactSourceSyntax.synWex nb067AlphaDummy085 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy083) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy085)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy084)))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0259 (f : SemanticCore.Var) : f ∈ {nb067AlphaDummy086 f} ∪ {nb067AlphaDummy087 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb067AlphaDummy088 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb067AlphaDummy088 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb067AlphaDummy087 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0260 : nb067AlphaDummy000 ∈ {nb067AlphaDummy163} ∪ {nb067AlphaDummy164} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy163)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0261 (f : SemanticCore.Var) : f ∈ {nb067AlphaDummy165 f} ∪ {nb067AlphaDummy166 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb067AlphaDummy165 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0262 : nb067AlphaDummy000 ∈ (SemanticCore.Class.cv nb067AlphaDummy000).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0263 (f : SemanticCore.Var) : f ∈ (SemanticCore.Class.cv f).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0264 : nb067AlphaDummy085 ∈ (SemanticCore.Class.cv nb067AlphaDummy085).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy084).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0265 : nb067AlphaDummy085 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy241 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy242 (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy241) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy241 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy242 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy241) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0266 (f : SemanticCore.Var) : nb067AlphaDummy088 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy088 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy087 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0267 (f : SemanticCore.Var) : nb067AlphaDummy088 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy243 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy244 f) (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy243 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy243 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy244 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy243 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0268 : nb067AlphaDummy085 ∈ (SemanticCore.Class.cab nb067AlphaDummy241 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy242 (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy241) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy241 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy242 (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy241) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0269 (f : SemanticCore.Var) : nb067AlphaDummy088 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy243 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy244 f) (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy243 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f)))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy243 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy244 f) (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy243 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0270 : nb067AlphaDummy242 ∈ (SemanticCore.Class.cv nb067AlphaDummy242).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0271 (f : SemanticCore.Var) : nb067AlphaDummy244 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy244 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0273 (f : SemanticCore.Var) : nb067AlphaDummy251 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy251 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy251 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy251 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0274 : nb067AlphaDummy249 ∈ (SemanticCore.Class.cv nb067AlphaDummy249).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0275 (f : SemanticCore.Var) : nb067AlphaDummy251 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy251 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0276 : nb067AlphaDummy256 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy256) (SemanticCore.Class.cv nb067AlphaDummy257)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy256) (SemanticCore.Class.cv nb067AlphaDummy257)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0277 (f : SemanticCore.Var) : nb067AlphaDummy259 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy259 f)) (SemanticCore.Class.cv (nb067AlphaDummy260 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy259 f)) (SemanticCore.Class.cv (nb067AlphaDummy260 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0278 : nb067AlphaDummy256 ∈ (SemanticCore.Class.cv nb067AlphaDummy256).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy257).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0279 (f : SemanticCore.Var) : nb067AlphaDummy259 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy259 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy260 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0280 : nb067AlphaDummy257 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy256) (SemanticCore.Class.cv nb067AlphaDummy257)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy256) (SemanticCore.Class.cv nb067AlphaDummy257)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0281 (f : SemanticCore.Var) : nb067AlphaDummy260 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy259 f)) (SemanticCore.Class.cv (nb067AlphaDummy260 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy259 f)) (SemanticCore.Class.cv (nb067AlphaDummy260 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0282 : nb067AlphaDummy257 ∈ (SemanticCore.Class.cv nb067AlphaDummy256).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy257).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0283 (f : SemanticCore.Var) : nb067AlphaDummy260 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy259 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy260 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0284 : nb067AlphaDummy256 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy256)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy257)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0285 (f : SemanticCore.Var) : nb067AlphaDummy259 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy259 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy260 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0286 : nb067AlphaDummy256 ∈ (SemanticCore.Class.cv nb067AlphaDummy256).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy256).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0287 (f : SemanticCore.Var) : nb067AlphaDummy259 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy259 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy259 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0288 : nb067AlphaDummy257 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy256)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy257)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0289 (f : SemanticCore.Var) : nb067AlphaDummy260 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy259 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy260 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0290 : nb067AlphaDummy257 ∈ (SemanticCore.Class.cv nb067AlphaDummy257).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy257).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0291 (f : SemanticCore.Var) : nb067AlphaDummy260 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy260 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy260 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0292 : nb067AlphaDummy084 ∈ (SemanticCore.Class.cv nb067AlphaDummy085).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy084).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0293 : nb067AlphaDummy084 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy241 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy242 (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy241) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy241 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy242 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy241) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0294 (f : SemanticCore.Var) : nb067AlphaDummy087 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy088 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy087 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0295 (f : SemanticCore.Var) : nb067AlphaDummy087 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy243 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy244 f) (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy243 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy243 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy244 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy243 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0296 : nb067AlphaDummy084 ∈ (SemanticCore.Class.cab nb067AlphaDummy241 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy242 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy241) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy241 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy242 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy241) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0297 (f : SemanticCore.Var) : nb067AlphaDummy087 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy243 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy244 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy243 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy243 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy244 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy243 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0299 (f : SemanticCore.Var) : nb067AlphaDummy244 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0300 : nb067AlphaDummy242 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0301 (f : SemanticCore.Var) : nb067AlphaDummy244 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0302 : nb067AlphaDummy278 ∈ (SemanticCore.Class.cv nb067AlphaDummy278).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy277).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0303 : nb067AlphaDummy278 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy281 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy282 (SemanticCore.Class.cv nb067AlphaDummy278) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy281) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy281 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy282 (SemanticCore.Class.cv nb067AlphaDummy277) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy281) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0304 (f : SemanticCore.Var) : nb067AlphaDummy280 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy280 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy279 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0305 (f : SemanticCore.Var) : nb067AlphaDummy280 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy283 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy284 f) (SemanticCore.Class.cv (nb067AlphaDummy280 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy283 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy283 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy284 f) (SemanticCore.Class.cv (nb067AlphaDummy279 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy283 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0306 : nb067AlphaDummy278 ∈ (SemanticCore.Class.cab nb067AlphaDummy281 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy282 (SemanticCore.Class.cv nb067AlphaDummy278) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy281) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy281 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy282 (SemanticCore.Class.cv nb067AlphaDummy278) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy281) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0307 (f : SemanticCore.Var) : nb067AlphaDummy280 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy283 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy284 f) (SemanticCore.Class.cv (nb067AlphaDummy280 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy283 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f)))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy283 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy284 f) (SemanticCore.Class.cv (nb067AlphaDummy280 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy283 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0308 : nb067AlphaDummy282 ∈ (SemanticCore.Class.cv nb067AlphaDummy282).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0309 (f : SemanticCore.Var) : nb067AlphaDummy284 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy284 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0311 (f : SemanticCore.Var) : nb067AlphaDummy291 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy291 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy291 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy291 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0312 : nb067AlphaDummy289 ∈ (SemanticCore.Class.cv nb067AlphaDummy289).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0313 (f : SemanticCore.Var) : nb067AlphaDummy291 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy291 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0314 : nb067AlphaDummy296 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy296) (SemanticCore.Class.cv nb067AlphaDummy297)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy296) (SemanticCore.Class.cv nb067AlphaDummy297)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0315 (f : SemanticCore.Var) : nb067AlphaDummy299 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy299 f)) (SemanticCore.Class.cv (nb067AlphaDummy300 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy299 f)) (SemanticCore.Class.cv (nb067AlphaDummy300 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0316 : nb067AlphaDummy296 ∈ (SemanticCore.Class.cv nb067AlphaDummy296).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy297).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0317 (f : SemanticCore.Var) : nb067AlphaDummy299 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy299 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy300 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0318 : nb067AlphaDummy297 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy296) (SemanticCore.Class.cv nb067AlphaDummy297)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy296) (SemanticCore.Class.cv nb067AlphaDummy297)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0319 (f : SemanticCore.Var) : nb067AlphaDummy300 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy299 f)) (SemanticCore.Class.cv (nb067AlphaDummy300 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy299 f)) (SemanticCore.Class.cv (nb067AlphaDummy300 f))).fv