Nominal proof certificates grouped in dependency order.

Certificates from NAR4C090C001Part010.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_392 (u : SemanticCore.Var) : nb090AlphaDummy308 u ≠ nb090AlphaDummy310 u

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_393 (u : SemanticCore.Var) : nb090AlphaDummy309 u ≠ nb090AlphaDummy310 u

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_394 (A : SemanticCore.Class) : nb090AlphaDummy317 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy306 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy306 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_395 (A : SemanticCore.Class) : nb090AlphaDummy313 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy306 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy307 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_396 (A : SemanticCore.Class) : nb090AlphaDummy319 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy307 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy307 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_397 (u : SemanticCore.Var) : nb090AlphaDummy318 u ∉ (SemanticCore.Class.cv (nb090AlphaDummy309 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy309 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_398 (u : SemanticCore.Var) : nb090AlphaDummy314 u ∉ (SemanticCore.Class.cv (nb090AlphaDummy309 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy310 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_399 (u : SemanticCore.Var) : nb090AlphaDummy320 u ∉ (SemanticCore.Class.cv (nb090AlphaDummy310 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy310 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_400 (A : SemanticCore.Class) : nb090AlphaDummy337 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy334 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy333 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_401 (A : SemanticCore.Class) : nb090AlphaDummy338 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy334 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy333 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_402 (A : SemanticCore.Class) : nb090AlphaDummy337 A ≠ nb090AlphaDummy338 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_403 (h : SemanticCore.Var) : nb090AlphaDummy339 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy336 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy335 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_404 (h : SemanticCore.Var) : nb090AlphaDummy340 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy336 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy335 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_405 (h : SemanticCore.Var) : nb090AlphaDummy339 h ≠ nb090AlphaDummy340 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_406 (A : SemanticCore.Class) : nb090AlphaDummy345 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy338 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_407 (A : SemanticCore.Class) : nb090AlphaDummy346 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy338 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_408 (A : SemanticCore.Class) : nb090AlphaDummy345 A ≠ nb090AlphaDummy346 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_409 (h : SemanticCore.Var) : nb090AlphaDummy347 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy340 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_410 (h : SemanticCore.Var) : nb090AlphaDummy348 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy340 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_411 (h : SemanticCore.Var) : nb090AlphaDummy347 h ≠ nb090AlphaDummy348 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_412 (A : SemanticCore.Class) : nb090AlphaDummy351 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy345 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_413 (A : SemanticCore.Class) : nb090AlphaDummy352 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy345 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_414 (A : SemanticCore.Class) : nb090AlphaDummy353 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy345 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_415 (A : SemanticCore.Class) : nb090AlphaDummy351 A ≠ nb090AlphaDummy352 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_416 (A : SemanticCore.Class) : nb090AlphaDummy351 A ≠ nb090AlphaDummy353 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_417 (A : SemanticCore.Class) : nb090AlphaDummy352 A ≠ nb090AlphaDummy353 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_418 (h : SemanticCore.Var) : nb090AlphaDummy354 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy347 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_419 (h : SemanticCore.Var) : nb090AlphaDummy355 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy347 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_420 (h : SemanticCore.Var) : nb090AlphaDummy356 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy347 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_421 (h : SemanticCore.Var) : nb090AlphaDummy354 h ≠ nb090AlphaDummy355 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_422 (h : SemanticCore.Var) : nb090AlphaDummy354 h ≠ nb090AlphaDummy356 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_423 (h : SemanticCore.Var) : nb090AlphaDummy355 h ≠ nb090AlphaDummy356 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_424 (A : SemanticCore.Class) : nb090AlphaDummy363 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy352 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy352 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_425 (A : SemanticCore.Class) : nb090AlphaDummy359 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy352 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy353 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_426 (A : SemanticCore.Class) : nb090AlphaDummy365 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy353 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy353 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_427 (h : SemanticCore.Var) : nb090AlphaDummy364 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy355 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy355 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_428 (h : SemanticCore.Var) : nb090AlphaDummy360 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy355 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy356 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_429 (h : SemanticCore.Var) : nb090AlphaDummy366 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy356 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy356 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_430 (A : SemanticCore.Class) : nb090AlphaDummy417 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy375 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_431 (v : SemanticCore.Var) : nb090AlphaDummy418 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy376 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_432 (A : SemanticCore.Class) : nb090AlphaDummy389 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy382 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_433 (A : SemanticCore.Class) : nb090AlphaDummy390 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy382 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_434 (A : SemanticCore.Class) : nb090AlphaDummy389 A ≠ nb090AlphaDummy390 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_435 (v : SemanticCore.Var) : nb090AlphaDummy391 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy384 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_436 (v : SemanticCore.Var) : nb090AlphaDummy392 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy384 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_437 (v : SemanticCore.Var) : nb090AlphaDummy391 v ≠ nb090AlphaDummy392 v

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_438 (A : SemanticCore.Class) : nb090AlphaDummy395 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy389 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_439 (A : SemanticCore.Class) : nb090AlphaDummy396 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy389 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_440 (A : SemanticCore.Class) : nb090AlphaDummy397 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy389 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_441 (A : SemanticCore.Class) : nb090AlphaDummy395 A ≠ nb090AlphaDummy396 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_442 (A : SemanticCore.Class) : nb090AlphaDummy395 A ≠ nb090AlphaDummy397 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_443 (A : SemanticCore.Class) : nb090AlphaDummy396 A ≠ nb090AlphaDummy397 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_444 (v : SemanticCore.Var) : nb090AlphaDummy398 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy391 v)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_445 (v : SemanticCore.Var) : nb090AlphaDummy399 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy391 v)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_446 (v : SemanticCore.Var) : nb090AlphaDummy400 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy391 v)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_447 (v : SemanticCore.Var) : nb090AlphaDummy398 v ≠ nb090AlphaDummy399 v

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_448 (v : SemanticCore.Var) : nb090AlphaDummy398 v ≠ nb090AlphaDummy400 v

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_449 (v : SemanticCore.Var) : nb090AlphaDummy399 v ≠ nb090AlphaDummy400 v

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_450 (A : SemanticCore.Class) : nb090AlphaDummy407 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy396 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy396 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_451 (A : SemanticCore.Class) : nb090AlphaDummy403 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy396 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy397 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_452 (A : SemanticCore.Class) : nb090AlphaDummy409 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy397 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy397 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_453 (v : SemanticCore.Var) : nb090AlphaDummy408 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy399 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy399 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_454 (v : SemanticCore.Var) : nb090AlphaDummy404 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy399 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy400 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_455 (v : SemanticCore.Var) : nb090AlphaDummy410 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy400 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy400 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_456 (A : SemanticCore.Class) : nb090AlphaDummy431 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy423 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy424 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_457 (A : SemanticCore.Class) : nb090AlphaDummy432 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy423 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy424 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_458 (A : SemanticCore.Class) : nb090AlphaDummy431 A ≠ nb090AlphaDummy432 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_459 (A : SemanticCore.Class) : nb090AlphaDummy467 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy423 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy425 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_460 (A : SemanticCore.Class) : nb090AlphaDummy468 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy423 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy425 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_461 (A : SemanticCore.Class) : nb090AlphaDummy467 A ≠ nb090AlphaDummy468 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_462 (A : SemanticCore.Class) : nb090AlphaDummy581 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy425 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy424 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_463 (A : SemanticCore.Class) : nb090AlphaDummy582 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy425 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy424 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_464 (A : SemanticCore.Class) : nb090AlphaDummy581 A ≠ nb090AlphaDummy582 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_465 (h : SemanticCore.Var) : nb090AlphaDummy433 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy426 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy427 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_466 (h : SemanticCore.Var) : nb090AlphaDummy434 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy426 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy427 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_467 (h : SemanticCore.Var) : nb090AlphaDummy433 h ≠ nb090AlphaDummy434 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_468 (h : SemanticCore.Var) : nb090AlphaDummy469 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy426 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy428 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_469 (h : SemanticCore.Var) : nb090AlphaDummy470 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy426 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy428 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_470 (h : SemanticCore.Var) : nb090AlphaDummy469 h ≠ nb090AlphaDummy470 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_471 (h : SemanticCore.Var) : nb090AlphaDummy583 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy428 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy427 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_472 (h : SemanticCore.Var) : nb090AlphaDummy584 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy428 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy427 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_473 (h : SemanticCore.Var) : nb090AlphaDummy583 h ≠ nb090AlphaDummy584 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_474 (A : SemanticCore.Class) : nb090AlphaDummy439 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy432 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_475 (A : SemanticCore.Class) : nb090AlphaDummy440 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy432 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_476 (A : SemanticCore.Class) : nb090AlphaDummy439 A ≠ nb090AlphaDummy440 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_477 (h : SemanticCore.Var) : nb090AlphaDummy441 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy434 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_478 (h : SemanticCore.Var) : nb090AlphaDummy442 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy434 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_479 (h : SemanticCore.Var) : nb090AlphaDummy441 h ≠ nb090AlphaDummy442 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_480 (A : SemanticCore.Class) : nb090AlphaDummy445 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy439 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_481 (A : SemanticCore.Class) : nb090AlphaDummy446 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy439 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_482 (A : SemanticCore.Class) : nb090AlphaDummy447 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy439 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_483 (A : SemanticCore.Class) : nb090AlphaDummy445 A ≠ nb090AlphaDummy446 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_484 (A : SemanticCore.Class) : nb090AlphaDummy445 A ≠ nb090AlphaDummy447 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_485 (A : SemanticCore.Class) : nb090AlphaDummy446 A ≠ nb090AlphaDummy447 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_486 (h : SemanticCore.Var) : nb090AlphaDummy448 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy441 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_487 (h : SemanticCore.Var) : nb090AlphaDummy449 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy441 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_488 (h : SemanticCore.Var) : nb090AlphaDummy450 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy441 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_489 (h : SemanticCore.Var) : nb090AlphaDummy448 h ≠ nb090AlphaDummy449 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_490 (h : SemanticCore.Var) : nb090AlphaDummy448 h ≠ nb090AlphaDummy450 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_491 (h : SemanticCore.Var) : nb090AlphaDummy449 h ≠ nb090AlphaDummy450 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_492 (A : SemanticCore.Class) : nb090AlphaDummy457 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy446 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy446 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_493 (A : SemanticCore.Class) : nb090AlphaDummy453 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy446 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy447 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_494 (A : SemanticCore.Class) : nb090AlphaDummy459 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy447 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy447 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_495 (h : SemanticCore.Var) : nb090AlphaDummy458 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy449 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy449 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_496 (h : SemanticCore.Var) : nb090AlphaDummy454 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy449 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy450 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_497 (h : SemanticCore.Var) : nb090AlphaDummy460 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy450 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy450 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_498 (A : SemanticCore.Class) : nb090AlphaDummy475 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy468 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_499 (A : SemanticCore.Class) : nb090AlphaDummy476 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy468 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_500 (A : SemanticCore.Class) : nb090AlphaDummy475 A ≠ nb090AlphaDummy476 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_501 (h : SemanticCore.Var) : nb090AlphaDummy477 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy470 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_502 (h : SemanticCore.Var) : nb090AlphaDummy478 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy470 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_503 (h : SemanticCore.Var) : nb090AlphaDummy477 h ≠ nb090AlphaDummy478 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_504 (A : SemanticCore.Class) : nb090AlphaDummy481 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy475 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_505 (A : SemanticCore.Class) : nb090AlphaDummy482 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy475 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_506 (A : SemanticCore.Class) : nb090AlphaDummy483 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy475 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_507 (A : SemanticCore.Class) : nb090AlphaDummy481 A ≠ nb090AlphaDummy482 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_508 (A : SemanticCore.Class) : nb090AlphaDummy481 A ≠ nb090AlphaDummy483 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_509 (A : SemanticCore.Class) : nb090AlphaDummy482 A ≠ nb090AlphaDummy483 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_510 (h : SemanticCore.Var) : nb090AlphaDummy484 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy477 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_511 (h : SemanticCore.Var) : nb090AlphaDummy485 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy477 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_512 (h : SemanticCore.Var) : nb090AlphaDummy486 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy477 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_513 (h : SemanticCore.Var) : nb090AlphaDummy484 h ≠ nb090AlphaDummy485 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_514 (h : SemanticCore.Var) : nb090AlphaDummy484 h ≠ nb090AlphaDummy486 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_515 (h : SemanticCore.Var) : nb090AlphaDummy485 h ≠ nb090AlphaDummy486 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_516 (A : SemanticCore.Class) : nb090AlphaDummy493 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy482 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy482 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_517 (A : SemanticCore.Class) : nb090AlphaDummy489 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy482 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy483 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_518 (A : SemanticCore.Class) : nb090AlphaDummy495 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy483 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy483 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_519 (h : SemanticCore.Var) : nb090AlphaDummy494 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy485 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy485 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_520 (h : SemanticCore.Var) : nb090AlphaDummy490 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy485 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy486 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_521 (h : SemanticCore.Var) : nb090AlphaDummy496 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy486 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy486 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_522 (A : SemanticCore.Class) : nb090AlphaDummy509 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy503 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy504 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_523 (A : SemanticCore.Class) : nb090AlphaDummy510 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy503 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy504 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_524 (A : SemanticCore.Class) : nb090AlphaDummy509 A ≠ nb090AlphaDummy510 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_525 (A : SemanticCore.Class) : nb090AlphaDummy545 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy504 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy503 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_526 (A : SemanticCore.Class) : nb090AlphaDummy546 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy504 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy503 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_527 (A : SemanticCore.Class) : nb090AlphaDummy545 A ≠ nb090AlphaDummy546 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_528 (h : SemanticCore.Var) : nb090AlphaDummy511 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy505 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy506 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_529 (h : SemanticCore.Var) : nb090AlphaDummy512 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy505 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy506 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_530 (h : SemanticCore.Var) : nb090AlphaDummy511 h ≠ nb090AlphaDummy512 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_531 (h : SemanticCore.Var) : nb090AlphaDummy547 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy506 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy505 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_532 (h : SemanticCore.Var) : nb090AlphaDummy548 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy506 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy505 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_533 (h : SemanticCore.Var) : nb090AlphaDummy547 h ≠ nb090AlphaDummy548 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_534 (A : SemanticCore.Class) : nb090AlphaDummy517 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy510 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_535 (A : SemanticCore.Class) : nb090AlphaDummy518 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy510 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_536 (A : SemanticCore.Class) : nb090AlphaDummy517 A ≠ nb090AlphaDummy518 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_537 (h : SemanticCore.Var) : nb090AlphaDummy519 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy512 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_538 (h : SemanticCore.Var) : nb090AlphaDummy520 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy512 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_539 (h : SemanticCore.Var) : nb090AlphaDummy519 h ≠ nb090AlphaDummy520 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_540 (A : SemanticCore.Class) : nb090AlphaDummy523 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy517 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_541 (A : SemanticCore.Class) : nb090AlphaDummy524 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy517 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

Certificates from NAR4C090C001Part011.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_542 (A : SemanticCore.Class) : nb090AlphaDummy525 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy517 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_543 (A : SemanticCore.Class) : nb090AlphaDummy523 A ≠ nb090AlphaDummy524 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_544 (A : SemanticCore.Class) : nb090AlphaDummy523 A ≠ nb090AlphaDummy525 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_545 (A : SemanticCore.Class) : nb090AlphaDummy524 A ≠ nb090AlphaDummy525 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_546 (h : SemanticCore.Var) : nb090AlphaDummy526 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy519 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_547 (h : SemanticCore.Var) : nb090AlphaDummy527 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy519 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_548 (h : SemanticCore.Var) : nb090AlphaDummy528 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy519 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_549 (h : SemanticCore.Var) : nb090AlphaDummy526 h ≠ nb090AlphaDummy527 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_550 (h : SemanticCore.Var) : nb090AlphaDummy526 h ≠ nb090AlphaDummy528 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_551 (h : SemanticCore.Var) : nb090AlphaDummy527 h ≠ nb090AlphaDummy528 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_552 (A : SemanticCore.Class) : nb090AlphaDummy535 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy524 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy524 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_553 (A : SemanticCore.Class) : nb090AlphaDummy531 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy524 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy525 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_554 (A : SemanticCore.Class) : nb090AlphaDummy537 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy525 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy525 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_555 (h : SemanticCore.Var) : nb090AlphaDummy536 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy527 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy527 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_556 (h : SemanticCore.Var) : nb090AlphaDummy532 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy527 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy528 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_557 (h : SemanticCore.Var) : nb090AlphaDummy538 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy528 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy528 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_558 (A : SemanticCore.Class) : nb090AlphaDummy553 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy546 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_559 (A : SemanticCore.Class) : nb090AlphaDummy554 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy546 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_560 (A : SemanticCore.Class) : nb090AlphaDummy553 A ≠ nb090AlphaDummy554 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_561 (h : SemanticCore.Var) : nb090AlphaDummy555 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy548 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_562 (h : SemanticCore.Var) : nb090AlphaDummy556 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy548 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_563 (h : SemanticCore.Var) : nb090AlphaDummy555 h ≠ nb090AlphaDummy556 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_564 (A : SemanticCore.Class) : nb090AlphaDummy559 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy553 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_565 (A : SemanticCore.Class) : nb090AlphaDummy560 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy553 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_566 (A : SemanticCore.Class) : nb090AlphaDummy561 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy553 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_567 (A : SemanticCore.Class) : nb090AlphaDummy559 A ≠ nb090AlphaDummy560 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_568 (A : SemanticCore.Class) : nb090AlphaDummy559 A ≠ nb090AlphaDummy561 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_569 (A : SemanticCore.Class) : nb090AlphaDummy560 A ≠ nb090AlphaDummy561 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_570 (h : SemanticCore.Var) : nb090AlphaDummy562 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy555 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_571 (h : SemanticCore.Var) : nb090AlphaDummy563 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy555 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_572 (h : SemanticCore.Var) : nb090AlphaDummy564 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy555 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_573 (h : SemanticCore.Var) : nb090AlphaDummy562 h ≠ nb090AlphaDummy563 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_574 (h : SemanticCore.Var) : nb090AlphaDummy562 h ≠ nb090AlphaDummy564 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_575 (h : SemanticCore.Var) : nb090AlphaDummy563 h ≠ nb090AlphaDummy564 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_576 (A : SemanticCore.Class) : nb090AlphaDummy571 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy560 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy560 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_577 (A : SemanticCore.Class) : nb090AlphaDummy567 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy560 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy561 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_578 (A : SemanticCore.Class) : nb090AlphaDummy573 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy561 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy561 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_579 (h : SemanticCore.Var) : nb090AlphaDummy572 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy563 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy563 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_580 (h : SemanticCore.Var) : nb090AlphaDummy568 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy563 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy564 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_581 (h : SemanticCore.Var) : nb090AlphaDummy574 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy564 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy564 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_582 (A : SemanticCore.Class) : nb090AlphaDummy589 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy582 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_583 (A : SemanticCore.Class) : nb090AlphaDummy590 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy582 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_584 (A : SemanticCore.Class) : nb090AlphaDummy589 A ≠ nb090AlphaDummy590 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_585 (h : SemanticCore.Var) : nb090AlphaDummy591 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy584 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_586 (h : SemanticCore.Var) : nb090AlphaDummy592 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy584 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_587 (h : SemanticCore.Var) : nb090AlphaDummy591 h ≠ nb090AlphaDummy592 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_588 (A : SemanticCore.Class) : nb090AlphaDummy595 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy589 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_589 (A : SemanticCore.Class) : nb090AlphaDummy596 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy589 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_590 (A : SemanticCore.Class) : nb090AlphaDummy597 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy589 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_591 (A : SemanticCore.Class) : nb090AlphaDummy595 A ≠ nb090AlphaDummy596 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_592 (A : SemanticCore.Class) : nb090AlphaDummy595 A ≠ nb090AlphaDummy597 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_593 (A : SemanticCore.Class) : nb090AlphaDummy596 A ≠ nb090AlphaDummy597 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_594 (h : SemanticCore.Var) : nb090AlphaDummy598 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy591 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_595 (h : SemanticCore.Var) : nb090AlphaDummy599 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy591 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_596 (h : SemanticCore.Var) : nb090AlphaDummy600 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy591 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_597 (h : SemanticCore.Var) : nb090AlphaDummy598 h ≠ nb090AlphaDummy599 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_598 (h : SemanticCore.Var) : nb090AlphaDummy598 h ≠ nb090AlphaDummy600 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_599 (h : SemanticCore.Var) : nb090AlphaDummy599 h ≠ nb090AlphaDummy600 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_600 (A : SemanticCore.Class) : nb090AlphaDummy607 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy596 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy596 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_601 (A : SemanticCore.Class) : nb090AlphaDummy603 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy596 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy597 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_602 (A : SemanticCore.Class) : nb090AlphaDummy609 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy597 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy597 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_603 (h : SemanticCore.Var) : nb090AlphaDummy608 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy599 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy599 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_604 (h : SemanticCore.Var) : nb090AlphaDummy604 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy599 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy600 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_605 (h : SemanticCore.Var) : nb090AlphaDummy610 h ∉ (SemanticCore.Class.cv (nb090AlphaDummy600 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy600 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_606 (A : SemanticCore.Class) : nb090AlphaDummy625 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy618 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_607 (A : SemanticCore.Class) : nb090AlphaDummy626 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy618 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_608 (A : SemanticCore.Class) : nb090AlphaDummy625 A ≠ nb090AlphaDummy626 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_609 (v u h : SemanticCore.Var) : nb090AlphaDummy627 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy620 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_610 (v u h : SemanticCore.Var) : nb090AlphaDummy628 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy620 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_611 (v u h : SemanticCore.Var) : nb090AlphaDummy627 v u h ≠ nb090AlphaDummy628 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_612 (A : SemanticCore.Class) : nb090AlphaDummy631 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy625 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_613 (A : SemanticCore.Class) : nb090AlphaDummy632 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy625 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_614 (A : SemanticCore.Class) : nb090AlphaDummy633 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy625 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_615 (A : SemanticCore.Class) : nb090AlphaDummy631 A ≠ nb090AlphaDummy632 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_616 (A : SemanticCore.Class) : nb090AlphaDummy631 A ≠ nb090AlphaDummy633 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_617 (A : SemanticCore.Class) : nb090AlphaDummy632 A ≠ nb090AlphaDummy633 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_618 (v u h : SemanticCore.Var) : nb090AlphaDummy634 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy627 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_619 (v u h : SemanticCore.Var) : nb090AlphaDummy635 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy627 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_620 (v u h : SemanticCore.Var) : nb090AlphaDummy636 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy627 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_621 (v u h : SemanticCore.Var) : nb090AlphaDummy634 v u h ≠ nb090AlphaDummy635 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_622 (v u h : SemanticCore.Var) : nb090AlphaDummy634 v u h ≠ nb090AlphaDummy636 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_623 (v u h : SemanticCore.Var) : nb090AlphaDummy635 v u h ≠ nb090AlphaDummy636 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_624 (A : SemanticCore.Class) : nb090AlphaDummy643 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy632 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy632 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_625 (A : SemanticCore.Class) : nb090AlphaDummy639 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy632 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy633 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_626 (A : SemanticCore.Class) : nb090AlphaDummy645 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy633 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy633 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_627 (v u h : SemanticCore.Var) : nb090AlphaDummy644 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_628 (v u h : SemanticCore.Var) : nb090AlphaDummy640 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy636 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_629 (v u h : SemanticCore.Var) : nb090AlphaDummy646 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy636 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy636 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_630 (A : SemanticCore.Class) : nb090AlphaDummy697 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy655 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_631 (u : SemanticCore.Var) : nb090AlphaDummy698 u ∉ (SemanticCore.Class.cv (nb090AlphaDummy656 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_632 (A : SemanticCore.Class) : nb090AlphaDummy669 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy662 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_633 (A : SemanticCore.Class) : nb090AlphaDummy670 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy662 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_634 (A : SemanticCore.Class) : nb090AlphaDummy669 A ≠ nb090AlphaDummy670 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_635 (u : SemanticCore.Var) : nb090AlphaDummy671 u ∉ (SemanticCore.Class.cv (nb090AlphaDummy664 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_636 (u : SemanticCore.Var) : nb090AlphaDummy672 u ∉ (SemanticCore.Class.cv (nb090AlphaDummy664 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_637 (u : SemanticCore.Var) : nb090AlphaDummy671 u ≠ nb090AlphaDummy672 u

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_638 (A : SemanticCore.Class) : nb090AlphaDummy675 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy669 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_639 (A : SemanticCore.Class) : nb090AlphaDummy676 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy669 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_640 (A : SemanticCore.Class) : nb090AlphaDummy677 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy669 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_641 (A : SemanticCore.Class) : nb090AlphaDummy675 A ≠ nb090AlphaDummy676 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_642 (A : SemanticCore.Class) : nb090AlphaDummy675 A ≠ nb090AlphaDummy677 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_643 (A : SemanticCore.Class) : nb090AlphaDummy676 A ≠ nb090AlphaDummy677 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_644 (u : SemanticCore.Var) : nb090AlphaDummy678 u ∉ (SemanticCore.Class.cv (nb090AlphaDummy671 u)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_645 (u : SemanticCore.Var) : nb090AlphaDummy679 u ∉ (SemanticCore.Class.cv (nb090AlphaDummy671 u)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_646 (u : SemanticCore.Var) : nb090AlphaDummy680 u ∉ (SemanticCore.Class.cv (nb090AlphaDummy671 u)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_647 (u : SemanticCore.Var) : nb090AlphaDummy678 u ≠ nb090AlphaDummy679 u

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_648 (u : SemanticCore.Var) : nb090AlphaDummy678 u ≠ nb090AlphaDummy680 u

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_649 (u : SemanticCore.Var) : nb090AlphaDummy679 u ≠ nb090AlphaDummy680 u

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_650 (A : SemanticCore.Class) : nb090AlphaDummy687 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy676 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy676 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_651 (A : SemanticCore.Class) : nb090AlphaDummy683 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy676 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy677 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_652 (A : SemanticCore.Class) : nb090AlphaDummy689 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy677 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy677 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_653 (u : SemanticCore.Var) : nb090AlphaDummy688 u ∉ (SemanticCore.Class.cv (nb090AlphaDummy679 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy679 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_654 (u : SemanticCore.Var) : nb090AlphaDummy684 u ∉ (SemanticCore.Class.cv (nb090AlphaDummy679 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy680 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_655 (u : SemanticCore.Var) : nb090AlphaDummy690 u ∉ (SemanticCore.Class.cv (nb090AlphaDummy680 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy680 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_656 (A : SemanticCore.Class) : nb090AlphaDummy753 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy700 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_657 (A : SemanticCore.Class) : nb090AlphaDummy754 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy700 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_658 (A : SemanticCore.Class) : nb090AlphaDummy753 A ≠ nb090AlphaDummy754 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_659 (v u h : SemanticCore.Var) : nb090AlphaDummy755 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy702 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_660 (v u h : SemanticCore.Var) : nb090AlphaDummy756 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy702 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_661 (v u h : SemanticCore.Var) : nb090AlphaDummy755 v u h ≠ nb090AlphaDummy756 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_662 (A : SemanticCore.Class) : nb090AlphaDummy751 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy709 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_663 (v u h : SemanticCore.Var) : nb090AlphaDummy752 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy710 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_664 (A : SemanticCore.Class) : nb090AlphaDummy723 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy716 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_665 (A : SemanticCore.Class) : nb090AlphaDummy724 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy716 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_666 (A : SemanticCore.Class) : nb090AlphaDummy723 A ≠ nb090AlphaDummy724 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_667 (v u h : SemanticCore.Var) : nb090AlphaDummy725 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy718 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_668 (v u h : SemanticCore.Var) : nb090AlphaDummy726 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy718 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_669 (v u h : SemanticCore.Var) : nb090AlphaDummy725 v u h ≠ nb090AlphaDummy726 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_670 (A : SemanticCore.Class) : nb090AlphaDummy729 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy723 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_671 (A : SemanticCore.Class) : nb090AlphaDummy730 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy723 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_672 (A : SemanticCore.Class) : nb090AlphaDummy731 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy723 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_673 (A : SemanticCore.Class) : nb090AlphaDummy729 A ≠ nb090AlphaDummy730 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_674 (A : SemanticCore.Class) : nb090AlphaDummy729 A ≠ nb090AlphaDummy731 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_675 (A : SemanticCore.Class) : nb090AlphaDummy730 A ≠ nb090AlphaDummy731 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_676 (v u h : SemanticCore.Var) : nb090AlphaDummy732 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy725 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_677 (v u h : SemanticCore.Var) : nb090AlphaDummy733 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy725 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_678 (v u h : SemanticCore.Var) : nb090AlphaDummy734 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy725 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_679 (v u h : SemanticCore.Var) : nb090AlphaDummy732 v u h ≠ nb090AlphaDummy733 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_680 (v u h : SemanticCore.Var) : nb090AlphaDummy732 v u h ≠ nb090AlphaDummy734 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_681 (v u h : SemanticCore.Var) : nb090AlphaDummy733 v u h ≠ nb090AlphaDummy734 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_682 (A : SemanticCore.Class) : nb090AlphaDummy741 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy730 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy730 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_683 (A : SemanticCore.Class) : nb090AlphaDummy737 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy730 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy731 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_684 (A : SemanticCore.Class) : nb090AlphaDummy743 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy731 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy731 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_685 (v u h : SemanticCore.Var) : nb090AlphaDummy742 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_686 (v u h : SemanticCore.Var) : nb090AlphaDummy738 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy734 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_687 (v u h : SemanticCore.Var) : nb090AlphaDummy744 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy734 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy734 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_688 (A : SemanticCore.Class) : nb090AlphaDummy759 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy753 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_689 (A : SemanticCore.Class) : nb090AlphaDummy760 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy753 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_690 (A : SemanticCore.Class) : nb090AlphaDummy761 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy753 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_691 (A : SemanticCore.Class) : nb090AlphaDummy759 A ≠ nb090AlphaDummy760 A

Certificates from NAR4C090C001Part012.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_692 (A : SemanticCore.Class) : nb090AlphaDummy759 A ≠ nb090AlphaDummy761 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_693 (A : SemanticCore.Class) : nb090AlphaDummy760 A ≠ nb090AlphaDummy761 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_694 (v u h : SemanticCore.Var) : nb090AlphaDummy762 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy755 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_695 (v u h : SemanticCore.Var) : nb090AlphaDummy763 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy755 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_696 (v u h : SemanticCore.Var) : nb090AlphaDummy764 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy755 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_697 (v u h : SemanticCore.Var) : nb090AlphaDummy762 v u h ≠ nb090AlphaDummy763 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_698 (v u h : SemanticCore.Var) : nb090AlphaDummy762 v u h ≠ nb090AlphaDummy764 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_699 (v u h : SemanticCore.Var) : nb090AlphaDummy763 v u h ≠ nb090AlphaDummy764 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_700 (A : SemanticCore.Class) : nb090AlphaDummy771 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy760 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy760 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_701 (A : SemanticCore.Class) : nb090AlphaDummy767 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy760 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy761 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_702 (A : SemanticCore.Class) : nb090AlphaDummy773 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy761 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy761 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_703 (v u h : SemanticCore.Var) : nb090AlphaDummy772 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_704 (v u h : SemanticCore.Var) : nb090AlphaDummy768 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy764 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_705 (v u h : SemanticCore.Var) : nb090AlphaDummy774 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy764 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy764 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_706 (A : SemanticCore.Class) : nb090AlphaDummy821 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy779 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_707 (v u h : SemanticCore.Var) : nb090AlphaDummy822 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy780 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_708 (A : SemanticCore.Class) : nb090AlphaDummy793 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy786 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_709 (A : SemanticCore.Class) : nb090AlphaDummy794 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy786 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_710 (A : SemanticCore.Class) : nb090AlphaDummy793 A ≠ nb090AlphaDummy794 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_711 (v u h : SemanticCore.Var) : nb090AlphaDummy795 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy788 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_712 (v u h : SemanticCore.Var) : nb090AlphaDummy796 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy788 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_713 (v u h : SemanticCore.Var) : nb090AlphaDummy795 v u h ≠ nb090AlphaDummy796 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_714 (A : SemanticCore.Class) : nb090AlphaDummy799 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy793 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_715 (A : SemanticCore.Class) : nb090AlphaDummy800 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy793 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_716 (A : SemanticCore.Class) : nb090AlphaDummy801 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy793 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_717 (A : SemanticCore.Class) : nb090AlphaDummy799 A ≠ nb090AlphaDummy800 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_718 (A : SemanticCore.Class) : nb090AlphaDummy799 A ≠ nb090AlphaDummy801 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_719 (A : SemanticCore.Class) : nb090AlphaDummy800 A ≠ nb090AlphaDummy801 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_720 (v u h : SemanticCore.Var) : nb090AlphaDummy802 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy795 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_721 (v u h : SemanticCore.Var) : nb090AlphaDummy803 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy795 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_722 (v u h : SemanticCore.Var) : nb090AlphaDummy804 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy795 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_723 (v u h : SemanticCore.Var) : nb090AlphaDummy802 v u h ≠ nb090AlphaDummy803 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_724 (v u h : SemanticCore.Var) : nb090AlphaDummy802 v u h ≠ nb090AlphaDummy804 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_725 (v u h : SemanticCore.Var) : nb090AlphaDummy803 v u h ≠ nb090AlphaDummy804 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_726 (A : SemanticCore.Class) : nb090AlphaDummy811 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy800 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy800 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_727 (A : SemanticCore.Class) : nb090AlphaDummy807 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy800 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy801 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_728 (A : SemanticCore.Class) : nb090AlphaDummy813 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy801 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy801 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_729 (v u h : SemanticCore.Var) : nb090AlphaDummy812 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_730 (v u h : SemanticCore.Var) : nb090AlphaDummy808 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy804 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_731 (v u h : SemanticCore.Var) : nb090AlphaDummy814 v u h ∉ (SemanticCore.Class.cv (nb090AlphaDummy804 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy804 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_732 (A : SemanticCore.Class) : nb090AlphaDummy871 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy829 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_733 (v : SemanticCore.Var) : nb090AlphaDummy872 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy830 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_734 (A : SemanticCore.Class) : nb090AlphaDummy843 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy836 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_735 (A : SemanticCore.Class) : nb090AlphaDummy844 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy836 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_736 (A : SemanticCore.Class) : nb090AlphaDummy843 A ≠ nb090AlphaDummy844 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_737 (v : SemanticCore.Var) : nb090AlphaDummy845 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy838 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_738 (v : SemanticCore.Var) : nb090AlphaDummy846 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy838 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_739 (v : SemanticCore.Var) : nb090AlphaDummy845 v ≠ nb090AlphaDummy846 v

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_740 (A : SemanticCore.Class) : nb090AlphaDummy849 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy843 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_741 (A : SemanticCore.Class) : nb090AlphaDummy850 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy843 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_742 (A : SemanticCore.Class) : nb090AlphaDummy851 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy843 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_743 (A : SemanticCore.Class) : nb090AlphaDummy849 A ≠ nb090AlphaDummy850 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_744 (A : SemanticCore.Class) : nb090AlphaDummy849 A ≠ nb090AlphaDummy851 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_745 (A : SemanticCore.Class) : nb090AlphaDummy850 A ≠ nb090AlphaDummy851 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_746 (v : SemanticCore.Var) : nb090AlphaDummy852 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy845 v)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_747 (v : SemanticCore.Var) : nb090AlphaDummy853 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy845 v)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_748 (v : SemanticCore.Var) : nb090AlphaDummy854 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy845 v)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_749 (v : SemanticCore.Var) : nb090AlphaDummy852 v ≠ nb090AlphaDummy853 v

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_750 (v : SemanticCore.Var) : nb090AlphaDummy852 v ≠ nb090AlphaDummy854 v

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_751 (v : SemanticCore.Var) : nb090AlphaDummy853 v ≠ nb090AlphaDummy854 v

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_752 (A : SemanticCore.Class) : nb090AlphaDummy861 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy850 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy850 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_753 (A : SemanticCore.Class) : nb090AlphaDummy857 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy850 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy851 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_754 (A : SemanticCore.Class) : nb090AlphaDummy863 A ∉ (SemanticCore.Class.cv (nb090AlphaDummy851 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy851 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_755 (v : SemanticCore.Var) : nb090AlphaDummy862 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy853 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy853 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_756 (v : SemanticCore.Var) : nb090AlphaDummy858 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy853 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy854 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_757 (v : SemanticCore.Var) : nb090AlphaDummy864 v ∉ (SemanticCore.Class.cv (nb090AlphaDummy854 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy854 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_758 (h : SemanticCore.Var) : nb090AlphaDummy131 h ∉ (SemanticCore.Class.cv h).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_759 (h : SemanticCore.Var) : nb090AlphaDummy132 h ∉ (SemanticCore.Class.cv h).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_760 (h : SemanticCore.Var) : nb090AlphaDummy131 h ≠ nb090AlphaDummy132 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_761 (v u h : SemanticCore.Var) : nb090AlphaDummy708 v u h ∉ (SemanticCore.Class.cv h).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_762 (v u h : SemanticCore.Var) : nb090AlphaDummy778 v u h ∉ (SemanticCore.Class.cv h).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_763 (h : SemanticCore.Var) : nb090AlphaDummy052 h ∉ (SemanticCore.Class.cv h).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_764 (h : SemanticCore.Var) : nb090AlphaDummy053 h ∉ (SemanticCore.Class.cv h).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_765 (h : SemanticCore.Var) : nb090AlphaDummy054 h ∉ (SemanticCore.Class.cv h).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_766 (h : SemanticCore.Var) : nb090AlphaDummy052 h ≠ nb090AlphaDummy053 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_767 (h : SemanticCore.Var) : nb090AlphaDummy052 h ≠ nb090AlphaDummy054 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_768 (h : SemanticCore.Var) : nb090AlphaDummy053 h ≠ nb090AlphaDummy054 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_769 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∉ (SemanticCore.Class.cv h).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_770 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∉ (SemanticCore.Class.cv h).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_771 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ≠ nb090AlphaDummy044 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_772 (h : SemanticCore.Var) : nb090AlphaDummy335 h ∉ (SemanticCore.Class.cv h).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_773 (h : SemanticCore.Var) : nb090AlphaDummy336 h ∉ (SemanticCore.Class.cv h).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_774 (h : SemanticCore.Var) : nb090AlphaDummy335 h ≠ nb090AlphaDummy336 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_775 (u : SemanticCore.Var) : nb090AlphaDummy293 u ∉ (SemanticCore.Class.cv u).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy284 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_776 (u : SemanticCore.Var) : nb090AlphaDummy294 u ∉ (SemanticCore.Class.cv u).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy284 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_777 (u : SemanticCore.Var) : nb090AlphaDummy293 u ≠ nb090AlphaDummy294 u

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_778 (u : SemanticCore.Var) : nb090AlphaDummy663 u ∉ (SemanticCore.Class.cv u).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy654 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_779 (u : SemanticCore.Var) : nb090AlphaDummy664 u ∉ (SemanticCore.Class.cv u).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy654 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_780 (u : SemanticCore.Var) : nb090AlphaDummy663 u ≠ nb090AlphaDummy664 u

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_781 (v u : SemanticCore.Var) : nb090AlphaDummy007 v u ∉ (SemanticCore.Class.cv u).fv ∪ (SemanticCore.Class.cv v).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_782 (v u : SemanticCore.Var) : nb090AlphaDummy008 v u ∉ (SemanticCore.Class.cv u).fv ∪ (SemanticCore.Class.cv v).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_783 (v u : SemanticCore.Var) : nb090AlphaDummy007 v u ≠ nb090AlphaDummy008 v u

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_784 (v : SemanticCore.Var) : nb090AlphaDummy383 v ∉ (SemanticCore.Class.cv v).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy374 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_785 (v : SemanticCore.Var) : nb090AlphaDummy384 v ∉ (SemanticCore.Class.cv v).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy374 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_786 (v : SemanticCore.Var) : nb090AlphaDummy383 v ≠ nb090AlphaDummy384 v

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_787 (v : SemanticCore.Var) : nb090AlphaDummy837 v ∉ (SemanticCore.Class.cv v).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy828 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_788 (v : SemanticCore.Var) : nb090AlphaDummy838 v ∉ (SemanticCore.Class.cv v).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy828 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_789 (v : SemanticCore.Var) : nb090AlphaDummy837 v ≠ nb090AlphaDummy838 v

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_790 (A : SemanticCore.Class) : nb090AlphaDummy017 A ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy013 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy013 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy013 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_791 (v u : SemanticCore.Var) : nb090AlphaDummy018 v u ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy015 v u)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy015 v u)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy015 v u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_792 (A : SemanticCore.Class) : nb090AlphaDummy069 A ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy065 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy065 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy065 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_793 (h : SemanticCore.Var) : nb090AlphaDummy070 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy067 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy067 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy067 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_794 (A : SemanticCore.Class) : nb090AlphaDummy105 A ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy101 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy101 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy101 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_795 (h : SemanticCore.Var) : nb090AlphaDummy106 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy103 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy103 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy103 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_796 (A : SemanticCore.Class) : nb090AlphaDummy147 A ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy143 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy143 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy143 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_797 (h : SemanticCore.Var) : nb090AlphaDummy148 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy145 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy145 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy145 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_798 (A : SemanticCore.Class) : nb090AlphaDummy183 A ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy179 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy179 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy179 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_799 (h : SemanticCore.Var) : nb090AlphaDummy184 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy181 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy181 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy181 h)).fv

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_820 (A : SemanticCore.Class) : nb090AlphaDummy629 A ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy625 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy625 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy625 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_821 (v u h : SemanticCore.Var) : nb090AlphaDummy630 v u h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy627 v u h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy627 v u h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy627 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_822 (A : SemanticCore.Class) : nb090AlphaDummy673 A ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy669 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy669 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy669 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_823 (u : SemanticCore.Var) : nb090AlphaDummy674 u ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy671 u)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy671 u)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy671 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_824 (A : SemanticCore.Class) : nb090AlphaDummy727 A ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy723 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy723 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy723 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_825 (v u h : SemanticCore.Var) : nb090AlphaDummy728 v u h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy725 v u h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy725 v u h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy725 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_826 (A : SemanticCore.Class) : nb090AlphaDummy757 A ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy753 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy753 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy753 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_827 (v u h : SemanticCore.Var) : nb090AlphaDummy758 v u h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy755 v u h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy755 v u h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy755 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_828 (A : SemanticCore.Class) : nb090AlphaDummy797 A ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy793 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy793 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy793 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_829 (v u h : SemanticCore.Var) : nb090AlphaDummy798 v u h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy795 v u h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy795 v u h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy795 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_830 (A : SemanticCore.Class) : nb090AlphaDummy847 A ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy843 A)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy843 A)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy843 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_831 (v : SemanticCore.Var) : nb090AlphaDummy848 v ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy845 v)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy845 v)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy845 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_832 (A : SemanticCore.Class) : nb090AlphaDummy653 A ∉ Compiler.CompactSourceSyntax.synC1st.fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy001 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_833 (A : SemanticCore.Class) : nb090AlphaDummy827 A ∉ Compiler.CompactSourceSyntax.synC1st.fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy002 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_834 (u : SemanticCore.Var) : nb090AlphaDummy654 u ∉ Compiler.CompactSourceSyntax.synC1st.fv ∪ (SemanticCore.Class.cv u).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_835 (v : SemanticCore.Var) : nb090AlphaDummy828 v ∉ Compiler.CompactSourceSyntax.synC1st.fv ∪ (SemanticCore.Class.cv v).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_836 (A : SemanticCore.Class) : nb090AlphaDummy283 A ∉ Compiler.CompactSourceSyntax.synC2nd.fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy001 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_837 (A : SemanticCore.Class) : nb090AlphaDummy373 A ∉ Compiler.CompactSourceSyntax.synC2nd.fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy002 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_838 (u : SemanticCore.Var) : nb090AlphaDummy284 u ∉ Compiler.CompactSourceSyntax.synC2nd.fv ∪ (SemanticCore.Class.cv u).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_839 (v : SemanticCore.Var) : nb090AlphaDummy374 v ∉ Compiler.CompactSourceSyntax.synC2nd.fv ∪ (SemanticCore.Class.cv v).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_840 (A : SemanticCore.Class) : nb090AlphaDummy503 A ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_841 (A : SemanticCore.Class) : nb090AlphaDummy504 A ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv

Certificates from NAR4C090C001Part013.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_842 (A : SemanticCore.Class) : nb090AlphaDummy503 A ≠ nb090AlphaDummy504 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_843 (A : SemanticCore.Class) : nb090AlphaDummy423 A ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_844 (A : SemanticCore.Class) : nb090AlphaDummy424 A ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_845 (A : SemanticCore.Class) : nb090AlphaDummy425 A ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_846 (A : SemanticCore.Class) : nb090AlphaDummy423 A ≠ nb090AlphaDummy424 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_847 (A : SemanticCore.Class) : nb090AlphaDummy423 A ≠ nb090AlphaDummy425 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_848 (A : SemanticCore.Class) : nb090AlphaDummy424 A ≠ nb090AlphaDummy425 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_849 (A : SemanticCore.Class) : nb090AlphaDummy243 A ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_850 (A : SemanticCore.Class) : nb090AlphaDummy244 A ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_851 (A : SemanticCore.Class) : nb090AlphaDummy243 A ≠ nb090AlphaDummy244 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_852 (h : SemanticCore.Var) : nb090AlphaDummy505 h ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_853 (h : SemanticCore.Var) : nb090AlphaDummy506 h ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_854 (h : SemanticCore.Var) : nb090AlphaDummy505 h ≠ nb090AlphaDummy506 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_855 (h : SemanticCore.Var) : nb090AlphaDummy426 h ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_856 (h : SemanticCore.Var) : nb090AlphaDummy427 h ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_857 (h : SemanticCore.Var) : nb090AlphaDummy428 h ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_858 (h : SemanticCore.Var) : nb090AlphaDummy426 h ≠ nb090AlphaDummy427 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_859 (h : SemanticCore.Var) : nb090AlphaDummy426 h ≠ nb090AlphaDummy428 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_860 (h : SemanticCore.Var) : nb090AlphaDummy427 h ≠ nb090AlphaDummy428 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_861 (h : SemanticCore.Var) : nb090AlphaDummy245 h ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_862 (h : SemanticCore.Var) : nb090AlphaDummy246 h ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_863 (h : SemanticCore.Var) : nb090AlphaDummy245 h ≠ nb090AlphaDummy246 h

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_868 (A : SemanticCore.Class) : nb090AlphaDummy009 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy005 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy006 A) (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy005 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy006 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy005 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy006 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy005 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy006 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_869 (v u : SemanticCore.Var) : nb090AlphaDummy010 v u ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy007 v u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy008 v u) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy007 v u)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy007 v u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy008 v u) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy007 v u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_870 (A : SemanticCore.Class) : nb090AlphaDummy061 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy057 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy058 A) (SemanticCore.Class.cv (nb090AlphaDummy049 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy057 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy058 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy057 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy058 A) (SemanticCore.Class.cv (nb090AlphaDummy050 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy057 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy058 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_871 (h : SemanticCore.Var) : nb090AlphaDummy062 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy059 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy060 h) (SemanticCore.Class.cv (nb090AlphaDummy052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy059 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy060 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy059 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy060 h) (SemanticCore.Class.cv (nb090AlphaDummy053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy059 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy060 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_872 (A : SemanticCore.Class) : nb090AlphaDummy097 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy093 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy094 A) (SemanticCore.Class.cv (nb090AlphaDummy049 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy093 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy094 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy093 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy094 A) (SemanticCore.Class.cv (nb090AlphaDummy051 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy093 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy094 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_873 (h : SemanticCore.Var) : nb090AlphaDummy098 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy095 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy096 h) (SemanticCore.Class.cv (nb090AlphaDummy052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy095 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy096 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy095 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy096 h) (SemanticCore.Class.cv (nb090AlphaDummy054 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy095 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy096 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_874 (A : SemanticCore.Class) : nb090AlphaDummy139 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy135 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy136 A) (SemanticCore.Class.cv (nb090AlphaDummy129 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy135 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy135 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy136 A) (SemanticCore.Class.cv (nb090AlphaDummy130 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy135 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_875 (h : SemanticCore.Var) : nb090AlphaDummy140 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy137 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy138 h) (SemanticCore.Class.cv (nb090AlphaDummy131 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy137 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy137 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy138 h) (SemanticCore.Class.cv (nb090AlphaDummy132 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy137 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_876 (A : SemanticCore.Class) : nb090AlphaDummy175 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy171 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy172 A) (SemanticCore.Class.cv (nb090AlphaDummy130 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy171 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy172 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy171 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy172 A) (SemanticCore.Class.cv (nb090AlphaDummy129 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy171 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy172 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_877 (h : SemanticCore.Var) : nb090AlphaDummy176 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy173 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy174 h) (SemanticCore.Class.cv (nb090AlphaDummy132 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy173 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy174 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy173 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy174 h) (SemanticCore.Class.cv (nb090AlphaDummy131 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy173 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy174 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_898 (A : SemanticCore.Class) : nb090AlphaDummy621 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy617 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy618 A) (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy617 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy617 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy618 A) (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy617 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_899 (v u h : SemanticCore.Var) : nb090AlphaDummy622 v u h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy619 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy620 v u h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy619 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy619 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy620 v u h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy619 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_900 (A : SemanticCore.Class) : nb090AlphaDummy665 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy661 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy662 A) (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy661 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy661 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy662 A) (SemanticCore.Class.cv (nb090AlphaDummy653 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy661 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_901 (u : SemanticCore.Var) : nb090AlphaDummy666 u ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy663 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy664 u) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy663 u)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy663 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy664 u) (SemanticCore.Class.cv (nb090AlphaDummy654 u)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy663 u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_902 (A : SemanticCore.Class) : nb090AlphaDummy703 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_903 (v u h : SemanticCore.Var) : nb090AlphaDummy704 v u h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_904 (A : SemanticCore.Class) : nb090AlphaDummy719 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy715 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy716 A) (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy715 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy715 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy716 A) (SemanticCore.Class.cv (nb090AlphaDummy707 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy715 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_905 (v u h : SemanticCore.Var) : nb090AlphaDummy720 v u h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy717 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy718 v u h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy717 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy717 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy718 v u h) (SemanticCore.Class.cv (nb090AlphaDummy708 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy717 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_906 (A : SemanticCore.Class) : nb090AlphaDummy789 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy785 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy786 A) (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy785 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy785 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy786 A) (SemanticCore.Class.cv (nb090AlphaDummy777 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy785 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_907 (v u h : SemanticCore.Var) : nb090AlphaDummy790 v u h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy787 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy788 v u h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy787 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy787 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy788 v u h) (SemanticCore.Class.cv (nb090AlphaDummy778 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy787 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_908 (A : SemanticCore.Class) : nb090AlphaDummy839 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy835 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy836 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy835 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy835 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy836 A) (SemanticCore.Class.cv (nb090AlphaDummy827 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy835 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_909 (v : SemanticCore.Var) : nb090AlphaDummy840 v ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy837 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy838 v) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy837 v)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy837 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy838 v) (SemanticCore.Class.cv (nb090AlphaDummy828 v)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy837 v)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_910 (A : SemanticCore.Class) : nb090AlphaDummy029 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy020 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy021 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_911 (v u : SemanticCore.Var) : nb090AlphaDummy030 v u ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy023 v u))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy024 v u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_912 (A : SemanticCore.Class) : nb090AlphaDummy081 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy072 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy073 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_913 (h : SemanticCore.Var) : nb090AlphaDummy082 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy075 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy076 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_914 (A : SemanticCore.Class) : nb090AlphaDummy117 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy108 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy109 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_915 (h : SemanticCore.Var) : nb090AlphaDummy118 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy111 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy112 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_916 (A : SemanticCore.Class) : nb090AlphaDummy159 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy150 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy151 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_917 (h : SemanticCore.Var) : nb090AlphaDummy160 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy153 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy154 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_918 (A : SemanticCore.Class) : nb090AlphaDummy195 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy186 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy187 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_919 (h : SemanticCore.Var) : nb090AlphaDummy196 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy189 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy190 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_920 (A : SemanticCore.Class) : nb090AlphaDummy231 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy222 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy223 A))).fv

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