Nominal proof certificates grouped in dependency order.

Certificates from NAR4C078C001Part024.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0313 (g : SemanticCore.Var) : nb078AlphaDummy314 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy313 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy314 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0314 : nb078AlphaDummy310 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy310)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy311)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0315 (g : SemanticCore.Var) : nb078AlphaDummy313 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy313 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy314 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0316 : nb078AlphaDummy310 ∈ (SemanticCore.Class.cv nb078AlphaDummy310).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy310).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0317 (g : SemanticCore.Var) : nb078AlphaDummy313 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy313 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy313 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0318 : nb078AlphaDummy311 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy310)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy311)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0319 (g : SemanticCore.Var) : nb078AlphaDummy314 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy313 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy314 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0320 : nb078AlphaDummy311 ∈ (SemanticCore.Class.cv nb078AlphaDummy311).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy311).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0321 (g : SemanticCore.Var) : nb078AlphaDummy314 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy314 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy314 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0322 : nb078AlphaDummy288 ∈ (SemanticCore.Class.cv nb078AlphaDummy287).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy288).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0323 : nb078AlphaDummy288 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy295 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy296 (SemanticCore.Class.cv nb078AlphaDummy287) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy295) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy296)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy295 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy296 (SemanticCore.Class.cv nb078AlphaDummy288) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy295) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy296)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0324 (g : SemanticCore.Var) : nb078AlphaDummy291 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy290 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy291 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0325 (g : SemanticCore.Var) : nb078AlphaDummy291 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy297 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy298 g) (SemanticCore.Class.cv (nb078AlphaDummy290 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy297 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy297 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy298 g) (SemanticCore.Class.cv (nb078AlphaDummy291 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy297 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0326 : nb078AlphaDummy288 ∈ (SemanticCore.Class.cab nb078AlphaDummy295 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy296 (SemanticCore.Class.cv nb078AlphaDummy288) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy295) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy296)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy295 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy296 (SemanticCore.Class.cv nb078AlphaDummy288) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy295) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy296)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0327 (g : SemanticCore.Var) : nb078AlphaDummy291 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy297 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy298 g) (SemanticCore.Class.cv (nb078AlphaDummy291 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy297 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy297 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy298 g) (SemanticCore.Class.cv (nb078AlphaDummy291 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy297 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0329 (g : SemanticCore.Var) : nb078AlphaDummy298 g ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0331 (g : SemanticCore.Var) : nb078AlphaDummy298 g ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0332 : nb078AlphaDummy287 ∈ (SemanticCore.Class.cv nb078AlphaDummy287).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy289).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0333 : nb078AlphaDummy287 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy331 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy332 (SemanticCore.Class.cv nb078AlphaDummy287) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy331) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy332)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy331 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy332 (SemanticCore.Class.cv nb078AlphaDummy289) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy331) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy332)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0334 (g : SemanticCore.Var) : nb078AlphaDummy290 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy290 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy292 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0335 (g : SemanticCore.Var) : nb078AlphaDummy290 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy333 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy334 g) (SemanticCore.Class.cv (nb078AlphaDummy290 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy333 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy333 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy334 g) (SemanticCore.Class.cv (nb078AlphaDummy292 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy333 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0336 : nb078AlphaDummy287 ∈ (SemanticCore.Class.cab nb078AlphaDummy331 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy332 (SemanticCore.Class.cv nb078AlphaDummy287) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy331) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy332))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy331 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy332 (SemanticCore.Class.cv nb078AlphaDummy287) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy331) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy332))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0337 (g : SemanticCore.Var) : nb078AlphaDummy290 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy333 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy334 g) (SemanticCore.Class.cv (nb078AlphaDummy290 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy333 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy333 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy334 g) (SemanticCore.Class.cv (nb078AlphaDummy290 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy333 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0338 : nb078AlphaDummy332 ∈ (SemanticCore.Class.cv nb078AlphaDummy332).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0339 (g : SemanticCore.Var) : nb078AlphaDummy334 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy334 g)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0341 (g : SemanticCore.Var) : nb078AlphaDummy341 g ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy341 g)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy341 g)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy341 g)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0343 (g : SemanticCore.Var) : nb078AlphaDummy341 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy341 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0344 : nb078AlphaDummy346 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy346) (SemanticCore.Class.cv nb078AlphaDummy347)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy346) (SemanticCore.Class.cv nb078AlphaDummy347)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0345 (g : SemanticCore.Var) : nb078AlphaDummy349 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy349 g)) (SemanticCore.Class.cv (nb078AlphaDummy350 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy349 g)) (SemanticCore.Class.cv (nb078AlphaDummy350 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0346 : nb078AlphaDummy346 ∈ (SemanticCore.Class.cv nb078AlphaDummy346).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy347).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0347 (g : SemanticCore.Var) : nb078AlphaDummy349 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy349 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy350 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0348 : nb078AlphaDummy347 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy346) (SemanticCore.Class.cv nb078AlphaDummy347)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy346) (SemanticCore.Class.cv nb078AlphaDummy347)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0349 (g : SemanticCore.Var) : nb078AlphaDummy350 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy349 g)) (SemanticCore.Class.cv (nb078AlphaDummy350 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy349 g)) (SemanticCore.Class.cv (nb078AlphaDummy350 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0350 : nb078AlphaDummy347 ∈ (SemanticCore.Class.cv nb078AlphaDummy346).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy347).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0351 (g : SemanticCore.Var) : nb078AlphaDummy350 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy349 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy350 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0352 : nb078AlphaDummy346 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy346)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy347)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0353 (g : SemanticCore.Var) : nb078AlphaDummy349 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy349 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy350 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0354 : nb078AlphaDummy346 ∈ (SemanticCore.Class.cv nb078AlphaDummy346).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy346).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0355 (g : SemanticCore.Var) : nb078AlphaDummy349 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy349 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy349 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0356 : nb078AlphaDummy347 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy346)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy347)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0357 (g : SemanticCore.Var) : nb078AlphaDummy350 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy349 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy350 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0358 : nb078AlphaDummy347 ∈ (SemanticCore.Class.cv nb078AlphaDummy347).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy347).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0359 (g : SemanticCore.Var) : nb078AlphaDummy350 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy350 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy350 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0360 : nb078AlphaDummy289 ∈ (SemanticCore.Class.cv nb078AlphaDummy287).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy289).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0361 : nb078AlphaDummy289 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy331 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy332 (SemanticCore.Class.cv nb078AlphaDummy287) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy331) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy332)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy331 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy332 (SemanticCore.Class.cv nb078AlphaDummy289) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy331) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy332)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0362 (g : SemanticCore.Var) : nb078AlphaDummy292 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy290 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy292 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0363 (g : SemanticCore.Var) : nb078AlphaDummy292 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy333 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy334 g) (SemanticCore.Class.cv (nb078AlphaDummy290 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy333 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy333 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy334 g) (SemanticCore.Class.cv (nb078AlphaDummy292 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy333 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0364 : nb078AlphaDummy289 ∈ (SemanticCore.Class.cab nb078AlphaDummy331 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy332 (SemanticCore.Class.cv nb078AlphaDummy289) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy331) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy332)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy331 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy332 (SemanticCore.Class.cv nb078AlphaDummy289) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy331) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy332)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0365 (g : SemanticCore.Var) : nb078AlphaDummy292 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy333 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy334 g) (SemanticCore.Class.cv (nb078AlphaDummy292 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy333 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy333 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy334 g) (SemanticCore.Class.cv (nb078AlphaDummy292 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy333 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0367 (g : SemanticCore.Var) : nb078AlphaDummy334 g ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0369 (g : SemanticCore.Var) : nb078AlphaDummy334 g ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0370 : nb078AlphaDummy367 ∈ {nb078AlphaDummy367} ∪ {nb078AlphaDummy368} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy368) (SemanticCore.Class.cv nb078AlphaDummy001) (SemanticCore.Class.cv nb078AlphaDummy367)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0371 (g : SemanticCore.Var) : nb078AlphaDummy369 g ∈ {nb078AlphaDummy369 g} ∪ {nb078AlphaDummy370 g} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy370 g)) (SemanticCore.Class.cv g) (SemanticCore.Class.cv (nb078AlphaDummy369 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0372 : nb078AlphaDummy368 ∈ {nb078AlphaDummy367} ∪ {nb078AlphaDummy368} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy368) (SemanticCore.Class.cv nb078AlphaDummy001) (SemanticCore.Class.cv nb078AlphaDummy367)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0373 (g : SemanticCore.Var) : nb078AlphaDummy370 g ∈ {nb078AlphaDummy369 g} ∪ {nb078AlphaDummy370 g} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy370 g)) (SemanticCore.Class.cv g) (SemanticCore.Class.cv (nb078AlphaDummy369 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0374 : nb078AlphaDummy367 ∈ (SemanticCore.Class.cv nb078AlphaDummy367).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy368).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0375 : nb078AlphaDummy367 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy373 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy374 (SemanticCore.Class.cv nb078AlphaDummy367) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy373) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy374)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy373 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy374 (SemanticCore.Class.cv nb078AlphaDummy368) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy373) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy374)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0376 (g : SemanticCore.Var) : nb078AlphaDummy369 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy369 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy370 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0377 (g : SemanticCore.Var) : nb078AlphaDummy369 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy375 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy376 g) (SemanticCore.Class.cv (nb078AlphaDummy369 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy375 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy375 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy376 g) (SemanticCore.Class.cv (nb078AlphaDummy370 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy375 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0378 : nb078AlphaDummy367 ∈ (SemanticCore.Class.cab nb078AlphaDummy373 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy374 (SemanticCore.Class.cv nb078AlphaDummy367) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy373) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy374))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy373 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy374 (SemanticCore.Class.cv nb078AlphaDummy367) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy373) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy374))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0379 (g : SemanticCore.Var) : nb078AlphaDummy369 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy375 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy376 g) (SemanticCore.Class.cv (nb078AlphaDummy369 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy375 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy375 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy376 g) (SemanticCore.Class.cv (nb078AlphaDummy369 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy375 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0380 : nb078AlphaDummy374 ∈ (SemanticCore.Class.cv nb078AlphaDummy374).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0381 (g : SemanticCore.Var) : nb078AlphaDummy376 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy376 g)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0383 (g : SemanticCore.Var) : nb078AlphaDummy383 g ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy383 g)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy383 g)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy383 g)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0385 (g : SemanticCore.Var) : nb078AlphaDummy383 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy383 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0386 : nb078AlphaDummy388 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy388) (SemanticCore.Class.cv nb078AlphaDummy389)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy388) (SemanticCore.Class.cv nb078AlphaDummy389)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0387 (g : SemanticCore.Var) : nb078AlphaDummy391 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy391 g)) (SemanticCore.Class.cv (nb078AlphaDummy392 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy391 g)) (SemanticCore.Class.cv (nb078AlphaDummy392 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0388 : nb078AlphaDummy388 ∈ (SemanticCore.Class.cv nb078AlphaDummy388).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy389).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0389 (g : SemanticCore.Var) : nb078AlphaDummy391 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy391 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy392 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0390 : nb078AlphaDummy389 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy388) (SemanticCore.Class.cv nb078AlphaDummy389)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy388) (SemanticCore.Class.cv nb078AlphaDummy389)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0391 (g : SemanticCore.Var) : nb078AlphaDummy392 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy391 g)) (SemanticCore.Class.cv (nb078AlphaDummy392 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy391 g)) (SemanticCore.Class.cv (nb078AlphaDummy392 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0392 : nb078AlphaDummy389 ∈ (SemanticCore.Class.cv nb078AlphaDummy388).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy389).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0393 (g : SemanticCore.Var) : nb078AlphaDummy392 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy391 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy392 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0394 : nb078AlphaDummy388 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy388)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy389)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0395 (g : SemanticCore.Var) : nb078AlphaDummy391 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy391 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy392 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0396 : nb078AlphaDummy388 ∈ (SemanticCore.Class.cv nb078AlphaDummy388).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy388).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0397 (g : SemanticCore.Var) : nb078AlphaDummy391 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy391 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy391 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0398 : nb078AlphaDummy389 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy388)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy389)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0399 (g : SemanticCore.Var) : nb078AlphaDummy392 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy391 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy392 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0400 : nb078AlphaDummy389 ∈ (SemanticCore.Class.cv nb078AlphaDummy389).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy389).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0401 (g : SemanticCore.Var) : nb078AlphaDummy392 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy392 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy392 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0402 : nb078AlphaDummy368 ∈ (SemanticCore.Class.cv nb078AlphaDummy367).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy368).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0403 : nb078AlphaDummy368 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy373 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy374 (SemanticCore.Class.cv nb078AlphaDummy367) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy373) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy374)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy373 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy374 (SemanticCore.Class.cv nb078AlphaDummy368) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy373) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy374)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0404 (g : SemanticCore.Var) : nb078AlphaDummy370 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy369 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy370 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0405 (g : SemanticCore.Var) : nb078AlphaDummy370 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy375 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy376 g) (SemanticCore.Class.cv (nb078AlphaDummy369 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy375 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy375 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy376 g) (SemanticCore.Class.cv (nb078AlphaDummy370 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy375 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0406 : nb078AlphaDummy368 ∈ (SemanticCore.Class.cab nb078AlphaDummy373 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy374 (SemanticCore.Class.cv nb078AlphaDummy368) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy373) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy374)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy373 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy374 (SemanticCore.Class.cv nb078AlphaDummy368) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy373) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy374)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0407 (g : SemanticCore.Var) : nb078AlphaDummy370 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy375 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy376 g) (SemanticCore.Class.cv (nb078AlphaDummy370 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy375 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy375 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy376 g) (SemanticCore.Class.cv (nb078AlphaDummy370 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy375 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0409 (g : SemanticCore.Var) : nb078AlphaDummy376 g ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0411 (g : SemanticCore.Var) : nb078AlphaDummy376 g ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0412 : nb078AlphaDummy368 ∈ (SemanticCore.Class.cv nb078AlphaDummy368).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy367).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0413 : nb078AlphaDummy368 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy409 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy410 (SemanticCore.Class.cv nb078AlphaDummy368) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy409) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy410)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy409 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy410 (SemanticCore.Class.cv nb078AlphaDummy367) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy409) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy410)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0414 (g : SemanticCore.Var) : nb078AlphaDummy370 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy370 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy369 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0415 (g : SemanticCore.Var) : nb078AlphaDummy370 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy411 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy412 g) (SemanticCore.Class.cv (nb078AlphaDummy370 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy411 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy411 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy412 g) (SemanticCore.Class.cv (nb078AlphaDummy369 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy411 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0416 : nb078AlphaDummy368 ∈ (SemanticCore.Class.cab nb078AlphaDummy409 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy410 (SemanticCore.Class.cv nb078AlphaDummy368) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy409) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy410))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy409 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy410 (SemanticCore.Class.cv nb078AlphaDummy368) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy409) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy410))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0417 (g : SemanticCore.Var) : nb078AlphaDummy370 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy411 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy412 g) (SemanticCore.Class.cv (nb078AlphaDummy370 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy411 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy411 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy412 g) (SemanticCore.Class.cv (nb078AlphaDummy370 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy411 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0418 : nb078AlphaDummy410 ∈ (SemanticCore.Class.cv nb078AlphaDummy410).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0419 (g : SemanticCore.Var) : nb078AlphaDummy412 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy412 g)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0421 (g : SemanticCore.Var) : nb078AlphaDummy419 g ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy419 g)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy419 g)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy419 g)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0423 (g : SemanticCore.Var) : nb078AlphaDummy419 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy419 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0424 : nb078AlphaDummy424 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy424) (SemanticCore.Class.cv nb078AlphaDummy425)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy424) (SemanticCore.Class.cv nb078AlphaDummy425)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0425 (g : SemanticCore.Var) : nb078AlphaDummy427 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy427 g)) (SemanticCore.Class.cv (nb078AlphaDummy428 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy427 g)) (SemanticCore.Class.cv (nb078AlphaDummy428 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0426 : nb078AlphaDummy424 ∈ (SemanticCore.Class.cv nb078AlphaDummy424).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy425).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0427 (g : SemanticCore.Var) : nb078AlphaDummy427 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy427 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy428 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0428 : nb078AlphaDummy425 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy424) (SemanticCore.Class.cv nb078AlphaDummy425)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy424) (SemanticCore.Class.cv nb078AlphaDummy425)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0429 (g : SemanticCore.Var) : nb078AlphaDummy428 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy427 g)) (SemanticCore.Class.cv (nb078AlphaDummy428 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy427 g)) (SemanticCore.Class.cv (nb078AlphaDummy428 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0430 : nb078AlphaDummy425 ∈ (SemanticCore.Class.cv nb078AlphaDummy424).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy425).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0431 (g : SemanticCore.Var) : nb078AlphaDummy428 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy427 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy428 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0432 : nb078AlphaDummy424 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy424)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy425)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0433 (g : SemanticCore.Var) : nb078AlphaDummy427 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy427 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy428 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0434 : nb078AlphaDummy424 ∈ (SemanticCore.Class.cv nb078AlphaDummy424).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy424).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0435 (g : SemanticCore.Var) : nb078AlphaDummy427 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy427 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy427 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0436 : nb078AlphaDummy425 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy424)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy425)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0437 (g : SemanticCore.Var) : nb078AlphaDummy428 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy427 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy428 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0438 : nb078AlphaDummy425 ∈ (SemanticCore.Class.cv nb078AlphaDummy425).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy425).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0439 (g : SemanticCore.Var) : nb078AlphaDummy428 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy428 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy428 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0440 : nb078AlphaDummy367 ∈ (SemanticCore.Class.cv nb078AlphaDummy368).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy367).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0441 : nb078AlphaDummy367 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy409 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy410 (SemanticCore.Class.cv nb078AlphaDummy368) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy409) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy410)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy409 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy410 (SemanticCore.Class.cv nb078AlphaDummy367) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy409) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy410)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0442 (g : SemanticCore.Var) : nb078AlphaDummy369 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy370 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy369 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0443 (g : SemanticCore.Var) : nb078AlphaDummy369 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy411 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy412 g) (SemanticCore.Class.cv (nb078AlphaDummy370 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy411 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy411 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy412 g) (SemanticCore.Class.cv (nb078AlphaDummy369 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy411 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0444 : nb078AlphaDummy367 ∈ (SemanticCore.Class.cab nb078AlphaDummy409 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy410 (SemanticCore.Class.cv nb078AlphaDummy367) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy409) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy410)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy409 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy410 (SemanticCore.Class.cv nb078AlphaDummy367) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy409) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy410)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0445 (g : SemanticCore.Var) : nb078AlphaDummy369 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy411 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy412 g) (SemanticCore.Class.cv (nb078AlphaDummy369 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy411 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy411 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy412 g) (SemanticCore.Class.cv (nb078AlphaDummy369 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy411 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0447 (g : SemanticCore.Var) : nb078AlphaDummy412 g ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0449 (g : SemanticCore.Var) : nb078AlphaDummy412 g ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g))).fv

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

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

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

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

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

Certificates from NAR4C078C001Part025.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0455 : nb078AlphaDummy001 ∈ {nb078AlphaDummy287} ∪ {nb078AlphaDummy288} ∪ (Compiler.CompactSourceSyntax.synWex nb078AlphaDummy289 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy287) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)) (SemanticCore.Class.cv nb078AlphaDummy289)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy289) (SemanticCore.Class.cv nb078AlphaDummy001) (SemanticCore.Class.cv nb078AlphaDummy288)))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0457 (g : SemanticCore.Var) : g ∈ {nb078AlphaDummy290 g} ∪ {nb078AlphaDummy291 g} ∪ (Compiler.CompactSourceSyntax.synWex (nb078AlphaDummy292 g) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy290 g)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)) (SemanticCore.Class.cv (nb078AlphaDummy292 g))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy292 g)) (SemanticCore.Class.cv g) (SemanticCore.Class.cv (nb078AlphaDummy291 g))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0458 : nb078AlphaDummy001 ∈ {nb078AlphaDummy367} ∪ {nb078AlphaDummy368} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy368) (SemanticCore.Class.cv nb078AlphaDummy001) (SemanticCore.Class.cv nb078AlphaDummy367)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0459 (g : SemanticCore.Var) : g ∈ {nb078AlphaDummy369 g} ∪ {nb078AlphaDummy370 g} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy370 g)) (SemanticCore.Class.cv g) (SemanticCore.Class.cv (nb078AlphaDummy369 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0460 : nb078AlphaDummy001 ∈ (SemanticCore.Class.cv nb078AlphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0461 (g : SemanticCore.Var) : g ∈ (SemanticCore.Class.cv g).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0462 : nb078AlphaDummy289 ∈ (SemanticCore.Class.cv nb078AlphaDummy289).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy288).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0463 : nb078AlphaDummy289 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy445 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy446 (SemanticCore.Class.cv nb078AlphaDummy289) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy445) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy446)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy445 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy446 (SemanticCore.Class.cv nb078AlphaDummy288) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy445) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy446)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0464 (g : SemanticCore.Var) : nb078AlphaDummy292 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy292 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy291 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0465 (g : SemanticCore.Var) : nb078AlphaDummy292 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy447 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy448 g) (SemanticCore.Class.cv (nb078AlphaDummy292 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy447 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy447 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy448 g) (SemanticCore.Class.cv (nb078AlphaDummy291 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy447 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0466 : nb078AlphaDummy289 ∈ (SemanticCore.Class.cab nb078AlphaDummy445 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy446 (SemanticCore.Class.cv nb078AlphaDummy289) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy445) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy446))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy445 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy446 (SemanticCore.Class.cv nb078AlphaDummy289) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy445) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy446))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0467 (g : SemanticCore.Var) : nb078AlphaDummy292 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy447 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy448 g) (SemanticCore.Class.cv (nb078AlphaDummy292 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy447 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy447 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy448 g) (SemanticCore.Class.cv (nb078AlphaDummy292 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy447 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0468 : nb078AlphaDummy446 ∈ (SemanticCore.Class.cv nb078AlphaDummy446).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0469 (g : SemanticCore.Var) : nb078AlphaDummy448 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy448 g)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0471 (g : SemanticCore.Var) : nb078AlphaDummy455 g ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy455 g)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy455 g)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy455 g)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0473 (g : SemanticCore.Var) : nb078AlphaDummy455 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy455 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0474 : nb078AlphaDummy460 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy460) (SemanticCore.Class.cv nb078AlphaDummy461)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy460) (SemanticCore.Class.cv nb078AlphaDummy461)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0475 (g : SemanticCore.Var) : nb078AlphaDummy463 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy463 g)) (SemanticCore.Class.cv (nb078AlphaDummy464 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy463 g)) (SemanticCore.Class.cv (nb078AlphaDummy464 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0476 : nb078AlphaDummy460 ∈ (SemanticCore.Class.cv nb078AlphaDummy460).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy461).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0477 (g : SemanticCore.Var) : nb078AlphaDummy463 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy463 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy464 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0478 : nb078AlphaDummy461 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy460) (SemanticCore.Class.cv nb078AlphaDummy461)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy460) (SemanticCore.Class.cv nb078AlphaDummy461)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0479 (g : SemanticCore.Var) : nb078AlphaDummy464 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy463 g)) (SemanticCore.Class.cv (nb078AlphaDummy464 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy463 g)) (SemanticCore.Class.cv (nb078AlphaDummy464 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0480 : nb078AlphaDummy461 ∈ (SemanticCore.Class.cv nb078AlphaDummy460).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy461).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0481 (g : SemanticCore.Var) : nb078AlphaDummy464 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy463 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy464 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0482 : nb078AlphaDummy460 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy460)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy461)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0483 (g : SemanticCore.Var) : nb078AlphaDummy463 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy463 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy464 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0484 : nb078AlphaDummy460 ∈ (SemanticCore.Class.cv nb078AlphaDummy460).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy460).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0485 (g : SemanticCore.Var) : nb078AlphaDummy463 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy463 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy463 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0486 : nb078AlphaDummy461 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy460)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy461)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0487 (g : SemanticCore.Var) : nb078AlphaDummy464 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy463 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy464 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0488 : nb078AlphaDummy461 ∈ (SemanticCore.Class.cv nb078AlphaDummy461).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy461).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0489 (g : SemanticCore.Var) : nb078AlphaDummy464 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy464 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy464 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0490 : nb078AlphaDummy288 ∈ (SemanticCore.Class.cv nb078AlphaDummy289).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy288).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0491 : nb078AlphaDummy288 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy445 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy446 (SemanticCore.Class.cv nb078AlphaDummy289) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy445) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy446)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy445 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy446 (SemanticCore.Class.cv nb078AlphaDummy288) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy445) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy446)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0492 (g : SemanticCore.Var) : nb078AlphaDummy291 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy292 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy291 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0493 (g : SemanticCore.Var) : nb078AlphaDummy291 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy447 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy448 g) (SemanticCore.Class.cv (nb078AlphaDummy292 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy447 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy447 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy448 g) (SemanticCore.Class.cv (nb078AlphaDummy291 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy447 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0494 : nb078AlphaDummy288 ∈ (SemanticCore.Class.cab nb078AlphaDummy445 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy446 (SemanticCore.Class.cv nb078AlphaDummy288) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy445) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy446)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy445 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy446 (SemanticCore.Class.cv nb078AlphaDummy288) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy445) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy446)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0495 (g : SemanticCore.Var) : nb078AlphaDummy291 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy447 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy448 g) (SemanticCore.Class.cv (nb078AlphaDummy291 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy447 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy447 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy448 g) (SemanticCore.Class.cv (nb078AlphaDummy291 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy447 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0497 (g : SemanticCore.Var) : nb078AlphaDummy448 g ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0499 (g : SemanticCore.Var) : nb078AlphaDummy448 g ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0500 : nb078AlphaDummy482 ∈ (SemanticCore.Class.cv nb078AlphaDummy482).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy481).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0501 : nb078AlphaDummy482 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy485 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy486 (SemanticCore.Class.cv nb078AlphaDummy482) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy485) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy486)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy485 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy486 (SemanticCore.Class.cv nb078AlphaDummy481) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy485) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy486)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0502 (g : SemanticCore.Var) : nb078AlphaDummy484 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy484 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy483 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0503 (g : SemanticCore.Var) : nb078AlphaDummy484 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy487 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy488 g) (SemanticCore.Class.cv (nb078AlphaDummy484 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy487 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy487 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy488 g) (SemanticCore.Class.cv (nb078AlphaDummy483 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy487 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0504 : nb078AlphaDummy482 ∈ (SemanticCore.Class.cab nb078AlphaDummy485 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy486 (SemanticCore.Class.cv nb078AlphaDummy482) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy485) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy486))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy485 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy486 (SemanticCore.Class.cv nb078AlphaDummy482) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy485) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy486))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0505 (g : SemanticCore.Var) : nb078AlphaDummy484 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy487 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy488 g) (SemanticCore.Class.cv (nb078AlphaDummy484 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy487 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy487 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy488 g) (SemanticCore.Class.cv (nb078AlphaDummy484 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy487 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0506 : nb078AlphaDummy486 ∈ (SemanticCore.Class.cv nb078AlphaDummy486).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0507 (g : SemanticCore.Var) : nb078AlphaDummy488 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy488 g)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0509 (g : SemanticCore.Var) : nb078AlphaDummy495 g ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy495 g)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy495 g)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy495 g)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0511 (g : SemanticCore.Var) : nb078AlphaDummy495 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy495 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0512 : nb078AlphaDummy500 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy500) (SemanticCore.Class.cv nb078AlphaDummy501)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy500) (SemanticCore.Class.cv nb078AlphaDummy501)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0513 (g : SemanticCore.Var) : nb078AlphaDummy503 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy503 g)) (SemanticCore.Class.cv (nb078AlphaDummy504 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy503 g)) (SemanticCore.Class.cv (nb078AlphaDummy504 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0514 : nb078AlphaDummy500 ∈ (SemanticCore.Class.cv nb078AlphaDummy500).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy501).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0515 (g : SemanticCore.Var) : nb078AlphaDummy503 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy503 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy504 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0516 : nb078AlphaDummy501 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy500) (SemanticCore.Class.cv nb078AlphaDummy501)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy500) (SemanticCore.Class.cv nb078AlphaDummy501)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0517 (g : SemanticCore.Var) : nb078AlphaDummy504 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy503 g)) (SemanticCore.Class.cv (nb078AlphaDummy504 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy503 g)) (SemanticCore.Class.cv (nb078AlphaDummy504 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0518 : nb078AlphaDummy501 ∈ (SemanticCore.Class.cv nb078AlphaDummy500).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy501).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0519 (g : SemanticCore.Var) : nb078AlphaDummy504 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy503 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy504 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0520 : nb078AlphaDummy500 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy500)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy501)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0521 (g : SemanticCore.Var) : nb078AlphaDummy503 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy503 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy504 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0522 : nb078AlphaDummy500 ∈ (SemanticCore.Class.cv nb078AlphaDummy500).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy500).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0523 (g : SemanticCore.Var) : nb078AlphaDummy503 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy503 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy503 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0524 : nb078AlphaDummy501 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy500)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy501)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0525 (g : SemanticCore.Var) : nb078AlphaDummy504 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy503 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy504 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0526 : nb078AlphaDummy501 ∈ (SemanticCore.Class.cv nb078AlphaDummy501).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy501).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0527 (g : SemanticCore.Var) : nb078AlphaDummy504 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy504 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy504 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0528 : nb078AlphaDummy481 ∈ (SemanticCore.Class.cv nb078AlphaDummy482).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy481).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0529 : nb078AlphaDummy481 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy485 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy486 (SemanticCore.Class.cv nb078AlphaDummy482) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy485) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy486)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy485 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy486 (SemanticCore.Class.cv nb078AlphaDummy481) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy485) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy486)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0530 (g : SemanticCore.Var) : nb078AlphaDummy483 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy484 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy483 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0531 (g : SemanticCore.Var) : nb078AlphaDummy483 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy487 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy488 g) (SemanticCore.Class.cv (nb078AlphaDummy484 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy487 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy487 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy488 g) (SemanticCore.Class.cv (nb078AlphaDummy483 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy487 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0532 : nb078AlphaDummy481 ∈ (SemanticCore.Class.cab nb078AlphaDummy485 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy486 (SemanticCore.Class.cv nb078AlphaDummy481) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy485) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy486)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy485 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy486 (SemanticCore.Class.cv nb078AlphaDummy481) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy485) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy486)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0533 (g : SemanticCore.Var) : nb078AlphaDummy483 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy487 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy488 g) (SemanticCore.Class.cv (nb078AlphaDummy483 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy487 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy487 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy488 g) (SemanticCore.Class.cv (nb078AlphaDummy483 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy487 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0535 (g : SemanticCore.Var) : nb078AlphaDummy488 g ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0537 (g : SemanticCore.Var) : nb078AlphaDummy488 g ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0538 : nb078AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0540 : nb078AlphaDummy526 ∈ (SemanticCore.Class.cv nb078AlphaDummy526).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy525).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0541 : nb078AlphaDummy526 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy529 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy530 (SemanticCore.Class.cv nb078AlphaDummy526) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy529) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy530)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy529 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy530 (SemanticCore.Class.cv nb078AlphaDummy525) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy529) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy530)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0542 (g : SemanticCore.Var) : nb078AlphaDummy528 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy528 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy527 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0543 (g : SemanticCore.Var) : nb078AlphaDummy528 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy531 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy532 g) (SemanticCore.Class.cv (nb078AlphaDummy528 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy531 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy531 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy532 g) (SemanticCore.Class.cv (nb078AlphaDummy527 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy531 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0544 : nb078AlphaDummy526 ∈ (SemanticCore.Class.cab nb078AlphaDummy529 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy530 (SemanticCore.Class.cv nb078AlphaDummy526) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy529) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy530))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy529 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy530 (SemanticCore.Class.cv nb078AlphaDummy526) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy529) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy530))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0545 (g : SemanticCore.Var) : nb078AlphaDummy528 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy531 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy532 g) (SemanticCore.Class.cv (nb078AlphaDummy528 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy531 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy531 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy532 g) (SemanticCore.Class.cv (nb078AlphaDummy528 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy531 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0546 : nb078AlphaDummy530 ∈ (SemanticCore.Class.cv nb078AlphaDummy530).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0547 (g : SemanticCore.Var) : nb078AlphaDummy532 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy532 g)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0549 (g : SemanticCore.Var) : nb078AlphaDummy539 g ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy539 g)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy539 g)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy539 g)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0551 (g : SemanticCore.Var) : nb078AlphaDummy539 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy539 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0552 : nb078AlphaDummy544 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy544) (SemanticCore.Class.cv nb078AlphaDummy545)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy544) (SemanticCore.Class.cv nb078AlphaDummy545)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0553 (g : SemanticCore.Var) : nb078AlphaDummy547 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy547 g)) (SemanticCore.Class.cv (nb078AlphaDummy548 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy547 g)) (SemanticCore.Class.cv (nb078AlphaDummy548 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0554 : nb078AlphaDummy544 ∈ (SemanticCore.Class.cv nb078AlphaDummy544).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy545).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0555 (g : SemanticCore.Var) : nb078AlphaDummy547 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy547 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy548 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0556 : nb078AlphaDummy545 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy544) (SemanticCore.Class.cv nb078AlphaDummy545)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy544) (SemanticCore.Class.cv nb078AlphaDummy545)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0557 (g : SemanticCore.Var) : nb078AlphaDummy548 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy547 g)) (SemanticCore.Class.cv (nb078AlphaDummy548 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy547 g)) (SemanticCore.Class.cv (nb078AlphaDummy548 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0558 : nb078AlphaDummy545 ∈ (SemanticCore.Class.cv nb078AlphaDummy544).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy545).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0559 (g : SemanticCore.Var) : nb078AlphaDummy548 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy547 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy548 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0560 : nb078AlphaDummy544 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy544)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy545)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0561 (g : SemanticCore.Var) : nb078AlphaDummy547 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy547 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy548 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0562 : nb078AlphaDummy544 ∈ (SemanticCore.Class.cv nb078AlphaDummy544).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy544).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0563 (g : SemanticCore.Var) : nb078AlphaDummy547 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy547 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy547 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0564 : nb078AlphaDummy545 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy544)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy545)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0565 (g : SemanticCore.Var) : nb078AlphaDummy548 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy547 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy548 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0566 : nb078AlphaDummy545 ∈ (SemanticCore.Class.cv nb078AlphaDummy545).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy545).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0567 (g : SemanticCore.Var) : nb078AlphaDummy548 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy548 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy548 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0568 : nb078AlphaDummy525 ∈ (SemanticCore.Class.cv nb078AlphaDummy526).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy525).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0569 : nb078AlphaDummy525 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy529 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy530 (SemanticCore.Class.cv nb078AlphaDummy526) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy529) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy530)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy529 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy530 (SemanticCore.Class.cv nb078AlphaDummy525) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy529) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy530)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0570 (g : SemanticCore.Var) : nb078AlphaDummy527 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy528 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy527 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0571 (g : SemanticCore.Var) : nb078AlphaDummy527 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy531 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy532 g) (SemanticCore.Class.cv (nb078AlphaDummy528 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy531 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy531 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy532 g) (SemanticCore.Class.cv (nb078AlphaDummy527 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy531 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0572 : nb078AlphaDummy525 ∈ (SemanticCore.Class.cab nb078AlphaDummy529 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy530 (SemanticCore.Class.cv nb078AlphaDummy525) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy529) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy530)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy529 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy530 (SemanticCore.Class.cv nb078AlphaDummy525) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy529) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy530)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0573 (g : SemanticCore.Var) : nb078AlphaDummy527 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy531 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy532 g) (SemanticCore.Class.cv (nb078AlphaDummy527 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy531 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy531 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy532 g) (SemanticCore.Class.cv (nb078AlphaDummy527 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy531 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0575 (g : SemanticCore.Var) : nb078AlphaDummy532 g ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0577 (g : SemanticCore.Var) : nb078AlphaDummy532 g ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0578 : nb078AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy001)) (SemanticCore.Class.cv nb078AlphaDummy003)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy001)) (SemanticCore.Class.cv nb078AlphaDummy003)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0579 (x g : SemanticCore.Var) : g ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv g)) (SemanticCore.Class.cv x)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv g)) (SemanticCore.Class.cv x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0580 : nb078AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy001)).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy003).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0581 (x g : SemanticCore.Var) : g ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv g)).fv ∪ (SemanticCore.Class.cv x).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0582 : nb078AlphaDummy001 ∈ (SemanticCore.Class.cv nb078AlphaDummy001).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0584 : nb078AlphaDummy003 ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy001)) (SemanticCore.Class.cv nb078AlphaDummy003)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy001)) (SemanticCore.Class.cv nb078AlphaDummy003)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0585 (x g : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv g)) (SemanticCore.Class.cv x)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv g)) (SemanticCore.Class.cv x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0586 : nb078AlphaDummy003 ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy001)).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy003).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0587 (x g : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv g)).fv ∪ (SemanticCore.Class.cv x).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0588 : nb078AlphaDummy569 ∈ {nb078AlphaDummy569} ∪ {nb078AlphaDummy570} ∪ (Compiler.CompactSourceSyntax.synWex nb078AlphaDummy571 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy569) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001))) (SemanticCore.Class.cv nb078AlphaDummy571)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy571) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)) (SemanticCore.Class.cv nb078AlphaDummy570)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0589 (g : SemanticCore.Var) : nb078AlphaDummy572 g ∈ {nb078AlphaDummy572 g} ∪ {nb078AlphaDummy573 g} ∪ (Compiler.CompactSourceSyntax.synWex (nb078AlphaDummy574 g) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy572 g)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g))) (SemanticCore.Class.cv (nb078AlphaDummy574 g))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy574 g)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)) (SemanticCore.Class.cv (nb078AlphaDummy573 g))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0590 : nb078AlphaDummy570 ∈ {nb078AlphaDummy569} ∪ {nb078AlphaDummy570} ∪ (Compiler.CompactSourceSyntax.synWex nb078AlphaDummy571 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy569) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001))) (SemanticCore.Class.cv nb078AlphaDummy571)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy571) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)) (SemanticCore.Class.cv nb078AlphaDummy570)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0591 (g : SemanticCore.Var) : nb078AlphaDummy573 g ∈ {nb078AlphaDummy572 g} ∪ {nb078AlphaDummy573 g} ∪ (Compiler.CompactSourceSyntax.synWex (nb078AlphaDummy574 g) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy572 g)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g))) (SemanticCore.Class.cv (nb078AlphaDummy574 g))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy574 g)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)) (SemanticCore.Class.cv (nb078AlphaDummy573 g))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0592 : nb078AlphaDummy569 ∈ (SemanticCore.Class.cv nb078AlphaDummy569).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy570).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0593 : nb078AlphaDummy569 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy577 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy578 (SemanticCore.Class.cv nb078AlphaDummy569) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy577) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy578)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy577 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy578 (SemanticCore.Class.cv nb078AlphaDummy570) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy577) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy578)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0594 (g : SemanticCore.Var) : nb078AlphaDummy572 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy572 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy573 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0595 (g : SemanticCore.Var) : nb078AlphaDummy572 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy579 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy580 g) (SemanticCore.Class.cv (nb078AlphaDummy572 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy579 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy580 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy579 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy580 g) (SemanticCore.Class.cv (nb078AlphaDummy573 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy579 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy580 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv