Nominal proof certificates grouped in dependency order.

Certificates from NAR4C077C001Part006.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_356 (F I : SemanticCore.Class) : nb077AlphaDummy305 F I ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy296 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy297 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_357 (x : SemanticCore.Var) : nb077AlphaDummy306 x ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy299 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy300 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_358 (F I : SemanticCore.Class) : nb077AlphaDummy335 F I ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy326 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy327 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_359 (x : SemanticCore.Var) : nb077AlphaDummy336 x ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy329 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy330 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_360 (F I : SemanticCore.Class) : nb077AlphaDummy051 F I ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_361 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy052 x F I ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_362 (F I : SemanticCore.Class) : nb077AlphaDummy099 F I ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_363 (x : SemanticCore.Var) : nb077AlphaDummy100 x ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_364 (F I : SemanticCore.Class) : nb077AlphaDummy135 F I ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_365 (x : SemanticCore.Var) : nb077AlphaDummy136 x ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_366 (F I : SemanticCore.Class) : nb077AlphaDummy179 F I ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_367 (x : SemanticCore.Var) : nb077AlphaDummy180 x ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_368 (F I : SemanticCore.Class) : nb077AlphaDummy215 F I ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_369 (x : SemanticCore.Var) : nb077AlphaDummy216 x ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_370 (F I : SemanticCore.Class) : nb077AlphaDummy251 F I ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_371 (x : SemanticCore.Var) : nb077AlphaDummy252 x ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_372 (F I : SemanticCore.Class) : nb077AlphaDummy291 F I ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_373 (x : SemanticCore.Var) : nb077AlphaDummy292 x ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_374 (F I : SemanticCore.Class) : nb077AlphaDummy343 F I ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_375 (x : SemanticCore.Var) : nb077AlphaDummy344 x ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_376 (F I : SemanticCore.Class) : nb077AlphaDummy013 F I ∉ (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) F) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy001 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_377 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy014 x F I ∉ (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) F) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy002 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_378 (F I : SemanticCore.Class) : nb077AlphaDummy139 F I ∉ (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)).fv ∪ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_379 (F I : SemanticCore.Class) : nb077AlphaDummy140 F I ∉ (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)).fv ∪ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_380 (F I : SemanticCore.Class) : nb077AlphaDummy141 F I ∉ (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)).fv ∪ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_distinct_381 (F I : SemanticCore.Class) : nb077AlphaDummy139 F I ≠ nb077AlphaDummy140 F I

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_distinct_382 (F I : SemanticCore.Class) : nb077AlphaDummy139 F I ≠ nb077AlphaDummy141 F I

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_distinct_383 (F I : SemanticCore.Class) : nb077AlphaDummy140 F I ≠ nb077AlphaDummy141 F I

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_384 (x : SemanticCore.Var) : nb077AlphaDummy142 x ∉ (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)).fv ∪ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_385 (x : SemanticCore.Var) : nb077AlphaDummy143 x ∉ (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)).fv ∪ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_386 (x : SemanticCore.Var) : nb077AlphaDummy144 x ∉ (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)).fv ∪ Compiler.CompactSourceSyntax.synC1st.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_distinct_387 (x : SemanticCore.Var) : nb077AlphaDummy142 x ≠ nb077AlphaDummy143 x

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_distinct_388 (x : SemanticCore.Var) : nb077AlphaDummy142 x ≠ nb077AlphaDummy144 x

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_distinct_389 (x : SemanticCore.Var) : nb077AlphaDummy143 x ≠ nb077AlphaDummy144 x

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_390 (F I : SemanticCore.Class) : nb077AlphaDummy039 F I ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy034 F I)) (SemanticCore.Class.cv (nb077AlphaDummy035 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy034 F I)) (SemanticCore.Class.cv (nb077AlphaDummy035 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_391 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy040 x F I ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy037 x F I)) (SemanticCore.Class.cv (nb077AlphaDummy038 x F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy037 x F I)) (SemanticCore.Class.cv (nb077AlphaDummy038 x F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_392 (F I : SemanticCore.Class) : nb077AlphaDummy087 F I ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy082 F I)) (SemanticCore.Class.cv (nb077AlphaDummy083 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy082 F I)) (SemanticCore.Class.cv (nb077AlphaDummy083 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_393 (x : SemanticCore.Var) : nb077AlphaDummy088 x ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy085 x)) (SemanticCore.Class.cv (nb077AlphaDummy086 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy085 x)) (SemanticCore.Class.cv (nb077AlphaDummy086 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_394 (F I : SemanticCore.Class) : nb077AlphaDummy123 F I ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy118 F I)) (SemanticCore.Class.cv (nb077AlphaDummy119 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy118 F I)) (SemanticCore.Class.cv (nb077AlphaDummy119 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_395 (x : SemanticCore.Var) : nb077AlphaDummy124 x ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy121 x)) (SemanticCore.Class.cv (nb077AlphaDummy122 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy121 x)) (SemanticCore.Class.cv (nb077AlphaDummy122 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_396 (F I : SemanticCore.Class) : nb077AlphaDummy167 F I ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy162 F I)) (SemanticCore.Class.cv (nb077AlphaDummy163 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy162 F I)) (SemanticCore.Class.cv (nb077AlphaDummy163 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_397 (x : SemanticCore.Var) : nb077AlphaDummy168 x ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy165 x)) (SemanticCore.Class.cv (nb077AlphaDummy166 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy165 x)) (SemanticCore.Class.cv (nb077AlphaDummy166 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_398 (F I : SemanticCore.Class) : nb077AlphaDummy203 F I ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy198 F I)) (SemanticCore.Class.cv (nb077AlphaDummy199 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy198 F I)) (SemanticCore.Class.cv (nb077AlphaDummy199 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_399 (x : SemanticCore.Var) : nb077AlphaDummy204 x ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy201 x)) (SemanticCore.Class.cv (nb077AlphaDummy202 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy201 x)) (SemanticCore.Class.cv (nb077AlphaDummy202 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_400 (F I : SemanticCore.Class) : nb077AlphaDummy239 F I ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy234 F I)) (SemanticCore.Class.cv (nb077AlphaDummy235 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy234 F I)) (SemanticCore.Class.cv (nb077AlphaDummy235 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_401 (x : SemanticCore.Var) : nb077AlphaDummy240 x ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy237 x)) (SemanticCore.Class.cv (nb077AlphaDummy238 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy237 x)) (SemanticCore.Class.cv (nb077AlphaDummy238 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_402 (F I : SemanticCore.Class) : nb077AlphaDummy279 F I ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy274 F I)) (SemanticCore.Class.cv (nb077AlphaDummy275 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy274 F I)) (SemanticCore.Class.cv (nb077AlphaDummy275 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_403 (x : SemanticCore.Var) : nb077AlphaDummy280 x ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy277 x)) (SemanticCore.Class.cv (nb077AlphaDummy278 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy277 x)) (SemanticCore.Class.cv (nb077AlphaDummy278 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_404 (F I : SemanticCore.Class) : nb077AlphaDummy301 F I ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy296 F I)) (SemanticCore.Class.cv (nb077AlphaDummy297 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy296 F I)) (SemanticCore.Class.cv (nb077AlphaDummy297 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_405 (x : SemanticCore.Var) : nb077AlphaDummy302 x ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy299 x)) (SemanticCore.Class.cv (nb077AlphaDummy300 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy299 x)) (SemanticCore.Class.cv (nb077AlphaDummy300 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_406 (F I : SemanticCore.Class) : nb077AlphaDummy331 F I ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy326 F I)) (SemanticCore.Class.cv (nb077AlphaDummy327 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy326 F I)) (SemanticCore.Class.cv (nb077AlphaDummy327 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_407 (x : SemanticCore.Var) : nb077AlphaDummy332 x ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy329 x)) (SemanticCore.Class.cv (nb077AlphaDummy330 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy329 x)) (SemanticCore.Class.cv (nb077AlphaDummy330 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_408 (F I : SemanticCore.Class) : nb077AlphaDummy055 F I ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) (Compiler.CompactSourceSyntax.synCcom F Compiler.CompactSourceSyntax.synC2nd))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) (Compiler.CompactSourceSyntax.synCcom F Compiler.CompactSourceSyntax.synC2nd))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_409 (x : SemanticCore.Var) (F : SemanticCore.Class) : nb077AlphaDummy056 x F ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) (Compiler.CompactSourceSyntax.synCcom F Compiler.CompactSourceSyntax.synC2nd))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) (Compiler.CompactSourceSyntax.synCcom F Compiler.CompactSourceSyntax.synC2nd))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_410 (F I : SemanticCore.Class) : nb077AlphaDummy011 F I ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) F) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) F) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_411 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy012 x F I ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) F) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) F) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_412 (F I : SemanticCore.Class) : nb077AlphaDummy007 F I ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_413 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy008 x F I ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_414 (F I : SemanticCore.Class) : nb077AlphaDummy053 F I ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_415 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy054 x F I ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_416 (F I : SemanticCore.Class) : nb077AlphaDummy101 F I ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_417 (x : SemanticCore.Var) : nb077AlphaDummy102 x ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_418 (F I : SemanticCore.Class) : nb077AlphaDummy137 F I ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_419 (x : SemanticCore.Var) : nb077AlphaDummy138 x ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_420 (F I : SemanticCore.Class) : nb077AlphaDummy181 F I ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_421 (x : SemanticCore.Var) : nb077AlphaDummy182 x ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_422 (F I : SemanticCore.Class) : nb077AlphaDummy217 F I ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_423 (x : SemanticCore.Var) : nb077AlphaDummy218 x ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_424 (F I : SemanticCore.Class) : nb077AlphaDummy253 F I ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_425 (x : SemanticCore.Var) : nb077AlphaDummy254 x ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_426 (F I : SemanticCore.Class) : nb077AlphaDummy293 F I ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_427 (x : SemanticCore.Var) : nb077AlphaDummy294 x ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_428 (F I : SemanticCore.Class) : nb077AlphaDummy345 F I ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_429 (x : SemanticCore.Var) : nb077AlphaDummy346 x ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_430 (F I : SemanticCore.Class) : nb077AlphaDummy015 F I ∉ (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) F).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy001 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_431 (F I : SemanticCore.Class) : nb077AlphaDummy016 F I ∉ (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) F).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy001 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_distinct_432 (F I : SemanticCore.Class) : nb077AlphaDummy015 F I ≠ nb077AlphaDummy016 F I

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_433 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy017 x F I ∉ (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) F).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy002 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_434 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy018 x F I ∉ (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) F).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy002 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_distinct_435 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy017 x F I ≠ nb077AlphaDummy018 x F I

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_436 (F I : SemanticCore.Class) : nb077AlphaDummy009 F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy001 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_437 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy010 x F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy002 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_438 (F I : SemanticCore.Class) : nb077AlphaDummy001 F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv ∪ (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) F).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_439 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy002 x F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv ∪ (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) F).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_440 (F I : SemanticCore.Class) : nb077AlphaDummy000 F I ∉ F.fv ∪ I.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_441 (F I : SemanticCore.Class) : nb077AlphaDummy255 F I ∉ {nb077AlphaDummy000 F I} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_442 (F I : SemanticCore.Class) : nb077AlphaDummy257 F I ∉ {nb077AlphaDummy000 F I} ∪ {nb077AlphaDummy255 F I} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy255 F I)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_443 (F I : SemanticCore.Class) : nb077AlphaDummy065 F I ∉ {nb077AlphaDummy059 F I} ∪ {nb077AlphaDummy060 F I} ∪ (Compiler.CompactSourceSyntax.synWex (nb077AlphaDummy061 F I) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy059 F I)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st) (SemanticCore.Class.cv (nb077AlphaDummy061 F I))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy061 F I)) (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (SemanticCore.Class.cv (nb077AlphaDummy060 F I))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_444 (x : SemanticCore.Var) : nb077AlphaDummy066 x ∉ {nb077AlphaDummy062 x} ∪ {nb077AlphaDummy063 x} ∪ (Compiler.CompactSourceSyntax.synWex (nb077AlphaDummy064 x) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy062 x)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st) (SemanticCore.Class.cv (nb077AlphaDummy064 x))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy064 x)) (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (SemanticCore.Class.cv (nb077AlphaDummy063 x))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_445 (F I : SemanticCore.Class) : nb077AlphaDummy145 F I ∉ {nb077AlphaDummy139 F I} ∪ {nb077AlphaDummy140 F I} ∪ (Compiler.CompactSourceSyntax.synWex (nb077AlphaDummy141 F I) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb077AlphaDummy141 F I))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Class.cv (nb077AlphaDummy140 F I))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_446 (x : SemanticCore.Var) : nb077AlphaDummy146 x ∉ {nb077AlphaDummy142 x} ∪ {nb077AlphaDummy143 x} ∪ (Compiler.CompactSourceSyntax.synWex (nb077AlphaDummy144 x) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy142 x)) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb077AlphaDummy144 x))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Class.cv (nb077AlphaDummy143 x))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_447 (x : SemanticCore.Var) : nb077AlphaDummy256 x ∉ {x} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_fresh_448 (x : SemanticCore.Var) : nb077AlphaDummy258 x ∉ {x} ∪ {nb077AlphaDummy256 x} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy256 x)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0000 (F I : SemanticCore.Class) : nb077AlphaDummy001 F I ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0001 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy002 x F I ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0002 (F I : SemanticCore.Class) : nb077AlphaDummy001 F I ∈ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy001 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0003 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy002 x F I ∈ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy002 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0004 (F I : SemanticCore.Class) : nb077AlphaDummy001 F I ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) F) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) F) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0005 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy002 x F I ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) F) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) F) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0006 (F I : SemanticCore.Class) : nb077AlphaDummy001 F I ∈ (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) F) (SemanticCore.Class.cv (nb077AlphaDummy001 F I))).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy001 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0007 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy002 x F I ∈ (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) F) (SemanticCore.Class.cv (nb077AlphaDummy002 x F I))).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy002 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0008 (F I : SemanticCore.Class) : nb077AlphaDummy001 F I ∈ (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) F).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy001 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0009 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy002 x F I ∈ (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) F).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy002 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0010 (F I : SemanticCore.Class) : nb077AlphaDummy016 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy016 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy015 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0011 (F I : SemanticCore.Class) : nb077AlphaDummy016 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy019 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy020 F I) (SemanticCore.Class.cv (nb077AlphaDummy016 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy019 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy019 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy020 F I) (SemanticCore.Class.cv (nb077AlphaDummy015 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy019 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0012 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy018 x F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy018 x F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy017 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0013 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy018 x F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy021 x F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy022 x F I) (SemanticCore.Class.cv (nb077AlphaDummy018 x F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy021 x F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy021 x F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy022 x F I) (SemanticCore.Class.cv (nb077AlphaDummy017 x F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy021 x F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0014 (F I : SemanticCore.Class) : nb077AlphaDummy016 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy019 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy020 F I) (SemanticCore.Class.cv (nb077AlphaDummy016 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy019 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy019 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy020 F I) (SemanticCore.Class.cv (nb077AlphaDummy016 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy019 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0015 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy018 x F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy021 x F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy022 x F I) (SemanticCore.Class.cv (nb077AlphaDummy018 x F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy021 x F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy021 x F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy022 x F I) (SemanticCore.Class.cv (nb077AlphaDummy018 x F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy021 x F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0016 (F I : SemanticCore.Class) : nb077AlphaDummy020 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy020 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0017 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy022 x F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy022 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0018 (F I : SemanticCore.Class) : nb077AlphaDummy027 F I ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy027 F I)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy027 F I)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy027 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0019 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy029 x F I ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy029 x F I)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy029 x F I)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy029 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0020 (F I : SemanticCore.Class) : nb077AlphaDummy027 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy027 F I)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0021 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy029 x F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy029 x F I)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0022 (F I : SemanticCore.Class) : nb077AlphaDummy034 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy034 F I)) (SemanticCore.Class.cv (nb077AlphaDummy035 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy034 F I)) (SemanticCore.Class.cv (nb077AlphaDummy035 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0023 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy037 x F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy037 x F I)) (SemanticCore.Class.cv (nb077AlphaDummy038 x F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy037 x F I)) (SemanticCore.Class.cv (nb077AlphaDummy038 x F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0024 (F I : SemanticCore.Class) : nb077AlphaDummy034 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy034 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy035 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0025 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy037 x F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy037 x F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy038 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0026 (F I : SemanticCore.Class) : nb077AlphaDummy035 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy034 F I)) (SemanticCore.Class.cv (nb077AlphaDummy035 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy034 F I)) (SemanticCore.Class.cv (nb077AlphaDummy035 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0027 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy038 x F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy037 x F I)) (SemanticCore.Class.cv (nb077AlphaDummy038 x F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy037 x F I)) (SemanticCore.Class.cv (nb077AlphaDummy038 x F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0028 (F I : SemanticCore.Class) : nb077AlphaDummy035 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy034 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy035 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0029 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy038 x F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy037 x F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy038 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0030 (F I : SemanticCore.Class) : nb077AlphaDummy034 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy034 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy035 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0031 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy037 x F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy037 x F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy038 x F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0032 (F I : SemanticCore.Class) : nb077AlphaDummy034 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy034 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy034 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0033 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy037 x F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy037 x F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy037 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0034 (F I : SemanticCore.Class) : nb077AlphaDummy035 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy034 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy035 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0035 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy038 x F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy037 x F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy038 x F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0036 (F I : SemanticCore.Class) : nb077AlphaDummy035 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy035 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy035 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0037 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy038 x F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy038 x F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy038 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0038 (F I : SemanticCore.Class) : nb077AlphaDummy015 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy016 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy015 F I)).fv

Certificates from NAR4C077C001Part007.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0039 (F I : SemanticCore.Class) : nb077AlphaDummy015 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy019 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy020 F I) (SemanticCore.Class.cv (nb077AlphaDummy016 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy019 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy019 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy020 F I) (SemanticCore.Class.cv (nb077AlphaDummy015 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy019 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0040 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy017 x F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy018 x F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy017 x F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0041 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy017 x F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy021 x F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy022 x F I) (SemanticCore.Class.cv (nb077AlphaDummy018 x F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy021 x F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy021 x F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy022 x F I) (SemanticCore.Class.cv (nb077AlphaDummy017 x F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy021 x F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0042 (F I : SemanticCore.Class) : nb077AlphaDummy015 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy019 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy020 F I) (SemanticCore.Class.cv (nb077AlphaDummy015 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy019 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy019 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy020 F I) (SemanticCore.Class.cv (nb077AlphaDummy015 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy019 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0043 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy017 x F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy021 x F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy022 x F I) (SemanticCore.Class.cv (nb077AlphaDummy017 x F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy021 x F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy021 x F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy022 x F I) (SemanticCore.Class.cv (nb077AlphaDummy017 x F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy021 x F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0044 (F I : SemanticCore.Class) : nb077AlphaDummy020 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0045 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy022 x F I ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0046 (F I : SemanticCore.Class) : nb077AlphaDummy020 F I ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy020 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0047 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy022 x F I ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy022 x F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0048 (F I : SemanticCore.Class) : nb077AlphaDummy059 F I ∈ {nb077AlphaDummy059 F I} ∪ {nb077AlphaDummy060 F I} ∪ (Compiler.CompactSourceSyntax.synWex (nb077AlphaDummy061 F I) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy059 F I)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st) (SemanticCore.Class.cv (nb077AlphaDummy061 F I))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy061 F I)) (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (SemanticCore.Class.cv (nb077AlphaDummy060 F I))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0049 (x : SemanticCore.Var) : nb077AlphaDummy062 x ∈ {nb077AlphaDummy062 x} ∪ {nb077AlphaDummy063 x} ∪ (Compiler.CompactSourceSyntax.synWex (nb077AlphaDummy064 x) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy062 x)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st) (SemanticCore.Class.cv (nb077AlphaDummy064 x))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy064 x)) (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (SemanticCore.Class.cv (nb077AlphaDummy063 x))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0050 (F I : SemanticCore.Class) : nb077AlphaDummy060 F I ∈ {nb077AlphaDummy059 F I} ∪ {nb077AlphaDummy060 F I} ∪ (Compiler.CompactSourceSyntax.synWex (nb077AlphaDummy061 F I) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy059 F I)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st) (SemanticCore.Class.cv (nb077AlphaDummy061 F I))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy061 F I)) (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (SemanticCore.Class.cv (nb077AlphaDummy060 F I))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0051 (x : SemanticCore.Var) : nb077AlphaDummy063 x ∈ {nb077AlphaDummy062 x} ∪ {nb077AlphaDummy063 x} ∪ (Compiler.CompactSourceSyntax.synWex (nb077AlphaDummy064 x) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy062 x)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st) (SemanticCore.Class.cv (nb077AlphaDummy064 x))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy064 x)) (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (SemanticCore.Class.cv (nb077AlphaDummy063 x))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0052 (F I : SemanticCore.Class) : nb077AlphaDummy059 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy059 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy060 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0053 (F I : SemanticCore.Class) : nb077AlphaDummy059 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy067 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy068 F I) (SemanticCore.Class.cv (nb077AlphaDummy059 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy067 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy067 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy068 F I) (SemanticCore.Class.cv (nb077AlphaDummy060 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy067 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0054 (x : SemanticCore.Var) : nb077AlphaDummy062 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy062 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy063 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0055 (x : SemanticCore.Var) : nb077AlphaDummy062 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy069 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy070 x) (SemanticCore.Class.cv (nb077AlphaDummy062 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy069 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy069 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy070 x) (SemanticCore.Class.cv (nb077AlphaDummy063 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy069 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0056 (F I : SemanticCore.Class) : nb077AlphaDummy059 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy067 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy068 F I) (SemanticCore.Class.cv (nb077AlphaDummy059 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy067 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy067 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy068 F I) (SemanticCore.Class.cv (nb077AlphaDummy059 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy067 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0057 (x : SemanticCore.Var) : nb077AlphaDummy062 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy069 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy070 x) (SemanticCore.Class.cv (nb077AlphaDummy062 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy069 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy069 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy070 x) (SemanticCore.Class.cv (nb077AlphaDummy062 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy069 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0058 (F I : SemanticCore.Class) : nb077AlphaDummy068 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy068 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0059 (x : SemanticCore.Var) : nb077AlphaDummy070 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy070 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0060 (F I : SemanticCore.Class) : nb077AlphaDummy075 F I ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy075 F I)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy075 F I)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy075 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0062 (F I : SemanticCore.Class) : nb077AlphaDummy075 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy075 F I)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0063 (x : SemanticCore.Var) : nb077AlphaDummy077 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy077 x)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0064 (F I : SemanticCore.Class) : nb077AlphaDummy082 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy082 F I)) (SemanticCore.Class.cv (nb077AlphaDummy083 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy082 F I)) (SemanticCore.Class.cv (nb077AlphaDummy083 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0065 (x : SemanticCore.Var) : nb077AlphaDummy085 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy085 x)) (SemanticCore.Class.cv (nb077AlphaDummy086 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy085 x)) (SemanticCore.Class.cv (nb077AlphaDummy086 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0066 (F I : SemanticCore.Class) : nb077AlphaDummy082 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy082 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy083 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0067 (x : SemanticCore.Var) : nb077AlphaDummy085 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy085 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy086 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0068 (F I : SemanticCore.Class) : nb077AlphaDummy083 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy082 F I)) (SemanticCore.Class.cv (nb077AlphaDummy083 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy082 F I)) (SemanticCore.Class.cv (nb077AlphaDummy083 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0069 (x : SemanticCore.Var) : nb077AlphaDummy086 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy085 x)) (SemanticCore.Class.cv (nb077AlphaDummy086 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy085 x)) (SemanticCore.Class.cv (nb077AlphaDummy086 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0070 (F I : SemanticCore.Class) : nb077AlphaDummy083 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy082 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy083 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0071 (x : SemanticCore.Var) : nb077AlphaDummy086 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy085 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy086 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0072 (F I : SemanticCore.Class) : nb077AlphaDummy082 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy082 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy083 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0073 (x : SemanticCore.Var) : nb077AlphaDummy085 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy085 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy086 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0074 (F I : SemanticCore.Class) : nb077AlphaDummy082 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy082 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy082 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0076 (F I : SemanticCore.Class) : nb077AlphaDummy083 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy082 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy083 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0077 (x : SemanticCore.Var) : nb077AlphaDummy086 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy085 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy086 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0078 (F I : SemanticCore.Class) : nb077AlphaDummy083 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy083 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy083 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0080 (F I : SemanticCore.Class) : nb077AlphaDummy060 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy059 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy060 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0081 (F I : SemanticCore.Class) : nb077AlphaDummy060 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy067 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy068 F I) (SemanticCore.Class.cv (nb077AlphaDummy059 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy067 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy067 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy068 F I) (SemanticCore.Class.cv (nb077AlphaDummy060 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy067 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0082 (x : SemanticCore.Var) : nb077AlphaDummy063 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy062 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy063 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0083 (x : SemanticCore.Var) : nb077AlphaDummy063 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy069 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy070 x) (SemanticCore.Class.cv (nb077AlphaDummy062 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy069 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy069 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy070 x) (SemanticCore.Class.cv (nb077AlphaDummy063 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy069 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0084 (F I : SemanticCore.Class) : nb077AlphaDummy060 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy067 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy068 F I) (SemanticCore.Class.cv (nb077AlphaDummy060 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy067 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy067 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy068 F I) (SemanticCore.Class.cv (nb077AlphaDummy060 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy067 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0085 (x : SemanticCore.Var) : nb077AlphaDummy063 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy069 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy070 x) (SemanticCore.Class.cv (nb077AlphaDummy063 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy069 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy069 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy070 x) (SemanticCore.Class.cv (nb077AlphaDummy063 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy069 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0086 (F I : SemanticCore.Class) : nb077AlphaDummy068 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0088 (F I : SemanticCore.Class) : nb077AlphaDummy068 F I ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0089 (x : SemanticCore.Var) : nb077AlphaDummy070 x ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0090 (F I : SemanticCore.Class) : nb077AlphaDummy059 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy059 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy061 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0091 (F I : SemanticCore.Class) : nb077AlphaDummy059 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy103 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy104 F I) (SemanticCore.Class.cv (nb077AlphaDummy059 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy103 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy103 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy104 F I) (SemanticCore.Class.cv (nb077AlphaDummy061 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy103 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0092 (x : SemanticCore.Var) : nb077AlphaDummy062 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy062 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy064 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0093 (x : SemanticCore.Var) : nb077AlphaDummy062 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy105 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy106 x) (SemanticCore.Class.cv (nb077AlphaDummy062 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy105 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy105 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy106 x) (SemanticCore.Class.cv (nb077AlphaDummy064 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy105 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0094 (F I : SemanticCore.Class) : nb077AlphaDummy059 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy103 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy104 F I) (SemanticCore.Class.cv (nb077AlphaDummy059 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy103 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy103 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy104 F I) (SemanticCore.Class.cv (nb077AlphaDummy059 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy103 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0095 (x : SemanticCore.Var) : nb077AlphaDummy062 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy105 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy106 x) (SemanticCore.Class.cv (nb077AlphaDummy062 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy105 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy105 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy106 x) (SemanticCore.Class.cv (nb077AlphaDummy062 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy105 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0096 (F I : SemanticCore.Class) : nb077AlphaDummy104 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy104 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0097 (x : SemanticCore.Var) : nb077AlphaDummy106 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy106 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0098 (F I : SemanticCore.Class) : nb077AlphaDummy111 F I ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy111 F I)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy111 F I)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy111 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0100 (F I : SemanticCore.Class) : nb077AlphaDummy111 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy111 F I)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0101 (x : SemanticCore.Var) : nb077AlphaDummy113 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy113 x)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0102 (F I : SemanticCore.Class) : nb077AlphaDummy118 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy118 F I)) (SemanticCore.Class.cv (nb077AlphaDummy119 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy118 F I)) (SemanticCore.Class.cv (nb077AlphaDummy119 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0103 (x : SemanticCore.Var) : nb077AlphaDummy121 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy121 x)) (SemanticCore.Class.cv (nb077AlphaDummy122 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy121 x)) (SemanticCore.Class.cv (nb077AlphaDummy122 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0104 (F I : SemanticCore.Class) : nb077AlphaDummy118 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy118 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy119 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0105 (x : SemanticCore.Var) : nb077AlphaDummy121 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy121 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy122 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0106 (F I : SemanticCore.Class) : nb077AlphaDummy119 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy118 F I)) (SemanticCore.Class.cv (nb077AlphaDummy119 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy118 F I)) (SemanticCore.Class.cv (nb077AlphaDummy119 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0107 (x : SemanticCore.Var) : nb077AlphaDummy122 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy121 x)) (SemanticCore.Class.cv (nb077AlphaDummy122 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy121 x)) (SemanticCore.Class.cv (nb077AlphaDummy122 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0108 (F I : SemanticCore.Class) : nb077AlphaDummy119 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy118 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy119 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0109 (x : SemanticCore.Var) : nb077AlphaDummy122 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy121 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy122 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0110 (F I : SemanticCore.Class) : nb077AlphaDummy118 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy118 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy119 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0111 (x : SemanticCore.Var) : nb077AlphaDummy121 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy121 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy122 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0112 (F I : SemanticCore.Class) : nb077AlphaDummy118 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy118 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy118 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0114 (F I : SemanticCore.Class) : nb077AlphaDummy119 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy118 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy119 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0115 (x : SemanticCore.Var) : nb077AlphaDummy122 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy121 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy122 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0116 (F I : SemanticCore.Class) : nb077AlphaDummy119 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy119 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy119 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0118 (F I : SemanticCore.Class) : nb077AlphaDummy061 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy059 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy061 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0119 (F I : SemanticCore.Class) : nb077AlphaDummy061 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy103 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy104 F I) (SemanticCore.Class.cv (nb077AlphaDummy059 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy103 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy103 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy104 F I) (SemanticCore.Class.cv (nb077AlphaDummy061 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy103 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0120 (x : SemanticCore.Var) : nb077AlphaDummy064 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy062 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy064 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0121 (x : SemanticCore.Var) : nb077AlphaDummy064 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy105 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy106 x) (SemanticCore.Class.cv (nb077AlphaDummy062 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy105 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy105 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy106 x) (SemanticCore.Class.cv (nb077AlphaDummy064 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy105 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0122 (F I : SemanticCore.Class) : nb077AlphaDummy061 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy103 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy104 F I) (SemanticCore.Class.cv (nb077AlphaDummy061 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy103 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy103 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy104 F I) (SemanticCore.Class.cv (nb077AlphaDummy061 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy103 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0123 (x : SemanticCore.Var) : nb077AlphaDummy064 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy105 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy106 x) (SemanticCore.Class.cv (nb077AlphaDummy064 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy105 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy105 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy106 x) (SemanticCore.Class.cv (nb077AlphaDummy064 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy105 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0124 (F I : SemanticCore.Class) : nb077AlphaDummy104 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0126 (F I : SemanticCore.Class) : nb077AlphaDummy104 F I ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy104 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0127 (x : SemanticCore.Var) : nb077AlphaDummy106 x ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy106 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0128 (F I : SemanticCore.Class) : nb077AlphaDummy139 F I ∈ {nb077AlphaDummy139 F I} ∪ {nb077AlphaDummy140 F I} ∪ (Compiler.CompactSourceSyntax.synWex (nb077AlphaDummy141 F I) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb077AlphaDummy141 F I))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Class.cv (nb077AlphaDummy140 F I))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0129 (x : SemanticCore.Var) : nb077AlphaDummy142 x ∈ {nb077AlphaDummy142 x} ∪ {nb077AlphaDummy143 x} ∪ (Compiler.CompactSourceSyntax.synWex (nb077AlphaDummy144 x) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy142 x)) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb077AlphaDummy144 x))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Class.cv (nb077AlphaDummy143 x))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0130 (F I : SemanticCore.Class) : nb077AlphaDummy140 F I ∈ {nb077AlphaDummy139 F I} ∪ {nb077AlphaDummy140 F I} ∪ (Compiler.CompactSourceSyntax.synWex (nb077AlphaDummy141 F I) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb077AlphaDummy141 F I))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Class.cv (nb077AlphaDummy140 F I))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0131 (x : SemanticCore.Var) : nb077AlphaDummy143 x ∈ {nb077AlphaDummy142 x} ∪ {nb077AlphaDummy143 x} ∪ (Compiler.CompactSourceSyntax.synWex (nb077AlphaDummy144 x) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy142 x)) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb077AlphaDummy144 x))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Class.cv (nb077AlphaDummy143 x))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0132 (F I : SemanticCore.Class) : nb077AlphaDummy139 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy139 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy140 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0133 (F I : SemanticCore.Class) : nb077AlphaDummy139 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy147 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy148 F I) (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy147 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy147 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy148 F I) (SemanticCore.Class.cv (nb077AlphaDummy140 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy147 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0134 (x : SemanticCore.Var) : nb077AlphaDummy142 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy142 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy143 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0135 (x : SemanticCore.Var) : nb077AlphaDummy142 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy149 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy150 x) (SemanticCore.Class.cv (nb077AlphaDummy142 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy149 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy149 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy150 x) (SemanticCore.Class.cv (nb077AlphaDummy143 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy149 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0136 (F I : SemanticCore.Class) : nb077AlphaDummy139 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy147 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy148 F I) (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy147 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy147 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy148 F I) (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy147 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0137 (x : SemanticCore.Var) : nb077AlphaDummy142 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy149 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy150 x) (SemanticCore.Class.cv (nb077AlphaDummy142 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy149 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy149 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy150 x) (SemanticCore.Class.cv (nb077AlphaDummy142 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy149 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0138 (F I : SemanticCore.Class) : nb077AlphaDummy148 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy148 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0139 (x : SemanticCore.Var) : nb077AlphaDummy150 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy150 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0140 (F I : SemanticCore.Class) : nb077AlphaDummy155 F I ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy155 F I)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy155 F I)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy155 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0142 (F I : SemanticCore.Class) : nb077AlphaDummy155 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy155 F I)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0143 (x : SemanticCore.Var) : nb077AlphaDummy157 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy157 x)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0144 (F I : SemanticCore.Class) : nb077AlphaDummy162 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy162 F I)) (SemanticCore.Class.cv (nb077AlphaDummy163 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy162 F I)) (SemanticCore.Class.cv (nb077AlphaDummy163 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0145 (x : SemanticCore.Var) : nb077AlphaDummy165 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy165 x)) (SemanticCore.Class.cv (nb077AlphaDummy166 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy165 x)) (SemanticCore.Class.cv (nb077AlphaDummy166 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0146 (F I : SemanticCore.Class) : nb077AlphaDummy162 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy162 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy163 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0147 (x : SemanticCore.Var) : nb077AlphaDummy165 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy165 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy166 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0148 (F I : SemanticCore.Class) : nb077AlphaDummy163 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy162 F I)) (SemanticCore.Class.cv (nb077AlphaDummy163 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy162 F I)) (SemanticCore.Class.cv (nb077AlphaDummy163 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0149 (x : SemanticCore.Var) : nb077AlphaDummy166 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy165 x)) (SemanticCore.Class.cv (nb077AlphaDummy166 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy165 x)) (SemanticCore.Class.cv (nb077AlphaDummy166 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0150 (F I : SemanticCore.Class) : nb077AlphaDummy163 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy162 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy163 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0151 (x : SemanticCore.Var) : nb077AlphaDummy166 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy165 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy166 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0152 (F I : SemanticCore.Class) : nb077AlphaDummy162 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy162 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy163 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0153 (x : SemanticCore.Var) : nb077AlphaDummy165 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy165 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy166 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0154 (F I : SemanticCore.Class) : nb077AlphaDummy162 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy162 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy162 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0156 (F I : SemanticCore.Class) : nb077AlphaDummy163 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy162 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy163 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0157 (x : SemanticCore.Var) : nb077AlphaDummy166 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy165 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy166 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0158 (F I : SemanticCore.Class) : nb077AlphaDummy163 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy163 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy163 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0160 (F I : SemanticCore.Class) : nb077AlphaDummy140 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy139 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy140 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0161 (F I : SemanticCore.Class) : nb077AlphaDummy140 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy147 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy148 F I) (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy147 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy147 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy148 F I) (SemanticCore.Class.cv (nb077AlphaDummy140 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy147 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0162 (x : SemanticCore.Var) : nb077AlphaDummy143 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy142 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy143 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0163 (x : SemanticCore.Var) : nb077AlphaDummy143 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy149 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy150 x) (SemanticCore.Class.cv (nb077AlphaDummy142 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy149 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy149 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy150 x) (SemanticCore.Class.cv (nb077AlphaDummy143 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy149 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0164 (F I : SemanticCore.Class) : nb077AlphaDummy140 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy147 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy148 F I) (SemanticCore.Class.cv (nb077AlphaDummy140 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy147 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy147 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy148 F I) (SemanticCore.Class.cv (nb077AlphaDummy140 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy147 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

Certificates from NAR4C077C001Part008.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0165 (x : SemanticCore.Var) : nb077AlphaDummy143 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy149 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy150 x) (SemanticCore.Class.cv (nb077AlphaDummy143 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy149 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy149 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy150 x) (SemanticCore.Class.cv (nb077AlphaDummy143 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy149 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0166 (F I : SemanticCore.Class) : nb077AlphaDummy148 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0168 (F I : SemanticCore.Class) : nb077AlphaDummy148 F I ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy148 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0169 (x : SemanticCore.Var) : nb077AlphaDummy150 x ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy150 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0170 (F I : SemanticCore.Class) : nb077AlphaDummy139 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy139 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy141 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0171 (F I : SemanticCore.Class) : nb077AlphaDummy139 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy183 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy184 F I) (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy183 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy183 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy184 F I) (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy183 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0172 (x : SemanticCore.Var) : nb077AlphaDummy142 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy142 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy144 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0173 (x : SemanticCore.Var) : nb077AlphaDummy142 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy185 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy186 x) (SemanticCore.Class.cv (nb077AlphaDummy142 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy185 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy185 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy186 x) (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy185 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0174 (F I : SemanticCore.Class) : nb077AlphaDummy139 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy183 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy184 F I) (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy183 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy183 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy184 F I) (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy183 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0175 (x : SemanticCore.Var) : nb077AlphaDummy142 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy185 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy186 x) (SemanticCore.Class.cv (nb077AlphaDummy142 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy185 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy185 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy186 x) (SemanticCore.Class.cv (nb077AlphaDummy142 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy185 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0176 (F I : SemanticCore.Class) : nb077AlphaDummy184 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy184 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0177 (x : SemanticCore.Var) : nb077AlphaDummy186 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy186 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0178 (F I : SemanticCore.Class) : nb077AlphaDummy191 F I ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy191 F I)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy191 F I)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy191 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0180 (F I : SemanticCore.Class) : nb077AlphaDummy191 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy191 F I)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0181 (x : SemanticCore.Var) : nb077AlphaDummy193 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy193 x)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0182 (F I : SemanticCore.Class) : nb077AlphaDummy198 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy198 F I)) (SemanticCore.Class.cv (nb077AlphaDummy199 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy198 F I)) (SemanticCore.Class.cv (nb077AlphaDummy199 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0183 (x : SemanticCore.Var) : nb077AlphaDummy201 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy201 x)) (SemanticCore.Class.cv (nb077AlphaDummy202 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy201 x)) (SemanticCore.Class.cv (nb077AlphaDummy202 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0184 (F I : SemanticCore.Class) : nb077AlphaDummy198 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy198 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy199 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0185 (x : SemanticCore.Var) : nb077AlphaDummy201 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy201 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy202 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0186 (F I : SemanticCore.Class) : nb077AlphaDummy199 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy198 F I)) (SemanticCore.Class.cv (nb077AlphaDummy199 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy198 F I)) (SemanticCore.Class.cv (nb077AlphaDummy199 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0187 (x : SemanticCore.Var) : nb077AlphaDummy202 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy201 x)) (SemanticCore.Class.cv (nb077AlphaDummy202 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy201 x)) (SemanticCore.Class.cv (nb077AlphaDummy202 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0188 (F I : SemanticCore.Class) : nb077AlphaDummy199 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy198 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy199 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0189 (x : SemanticCore.Var) : nb077AlphaDummy202 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy201 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy202 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0190 (F I : SemanticCore.Class) : nb077AlphaDummy198 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy198 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy199 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0191 (x : SemanticCore.Var) : nb077AlphaDummy201 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy201 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy202 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0192 (F I : SemanticCore.Class) : nb077AlphaDummy198 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy198 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy198 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0194 (F I : SemanticCore.Class) : nb077AlphaDummy199 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy198 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy199 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0195 (x : SemanticCore.Var) : nb077AlphaDummy202 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy201 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy202 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0196 (F I : SemanticCore.Class) : nb077AlphaDummy199 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy199 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy199 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0198 (F I : SemanticCore.Class) : nb077AlphaDummy141 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy139 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy141 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0199 (F I : SemanticCore.Class) : nb077AlphaDummy141 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy183 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy184 F I) (SemanticCore.Class.cv (nb077AlphaDummy139 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy183 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy183 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy184 F I) (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy183 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0200 (x : SemanticCore.Var) : nb077AlphaDummy144 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy142 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy144 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0201 (x : SemanticCore.Var) : nb077AlphaDummy144 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy185 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy186 x) (SemanticCore.Class.cv (nb077AlphaDummy142 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy185 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy185 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy186 x) (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy185 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0202 (F I : SemanticCore.Class) : nb077AlphaDummy141 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy183 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy184 F I) (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy183 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy183 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy184 F I) (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy183 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0203 (x : SemanticCore.Var) : nb077AlphaDummy144 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy185 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy186 x) (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy185 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy185 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy186 x) (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy185 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0204 (F I : SemanticCore.Class) : nb077AlphaDummy184 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0206 (F I : SemanticCore.Class) : nb077AlphaDummy184 F I ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy184 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0207 (x : SemanticCore.Var) : nb077AlphaDummy186 x ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy186 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0208 (F I : SemanticCore.Class) : nb077AlphaDummy141 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy141 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy140 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0209 (F I : SemanticCore.Class) : nb077AlphaDummy141 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy219 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy220 F I) (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy219 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy219 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy220 F I) (SemanticCore.Class.cv (nb077AlphaDummy140 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy219 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0210 (x : SemanticCore.Var) : nb077AlphaDummy144 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy144 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy143 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0211 (x : SemanticCore.Var) : nb077AlphaDummy144 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy221 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy222 x) (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy221 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy221 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy222 x) (SemanticCore.Class.cv (nb077AlphaDummy143 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy221 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0212 (F I : SemanticCore.Class) : nb077AlphaDummy141 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy219 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy220 F I) (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy219 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy219 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy220 F I) (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy219 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0213 (x : SemanticCore.Var) : nb077AlphaDummy144 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy221 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy222 x) (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy221 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy221 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy222 x) (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy221 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0214 (F I : SemanticCore.Class) : nb077AlphaDummy220 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy220 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0215 (x : SemanticCore.Var) : nb077AlphaDummy222 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy222 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0216 (F I : SemanticCore.Class) : nb077AlphaDummy227 F I ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy227 F I)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy227 F I)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy227 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0218 (F I : SemanticCore.Class) : nb077AlphaDummy227 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy227 F I)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0219 (x : SemanticCore.Var) : nb077AlphaDummy229 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy229 x)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0220 (F I : SemanticCore.Class) : nb077AlphaDummy234 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy234 F I)) (SemanticCore.Class.cv (nb077AlphaDummy235 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy234 F I)) (SemanticCore.Class.cv (nb077AlphaDummy235 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0221 (x : SemanticCore.Var) : nb077AlphaDummy237 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy237 x)) (SemanticCore.Class.cv (nb077AlphaDummy238 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy237 x)) (SemanticCore.Class.cv (nb077AlphaDummy238 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0222 (F I : SemanticCore.Class) : nb077AlphaDummy234 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy234 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy235 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0223 (x : SemanticCore.Var) : nb077AlphaDummy237 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy237 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy238 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0224 (F I : SemanticCore.Class) : nb077AlphaDummy235 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy234 F I)) (SemanticCore.Class.cv (nb077AlphaDummy235 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy234 F I)) (SemanticCore.Class.cv (nb077AlphaDummy235 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0225 (x : SemanticCore.Var) : nb077AlphaDummy238 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy237 x)) (SemanticCore.Class.cv (nb077AlphaDummy238 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy237 x)) (SemanticCore.Class.cv (nb077AlphaDummy238 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0226 (F I : SemanticCore.Class) : nb077AlphaDummy235 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy234 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy235 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0227 (x : SemanticCore.Var) : nb077AlphaDummy238 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy237 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy238 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0228 (F I : SemanticCore.Class) : nb077AlphaDummy234 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy234 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy235 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0229 (x : SemanticCore.Var) : nb077AlphaDummy237 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy237 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy238 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0230 (F I : SemanticCore.Class) : nb077AlphaDummy234 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy234 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy234 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0232 (F I : SemanticCore.Class) : nb077AlphaDummy235 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy234 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy235 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0233 (x : SemanticCore.Var) : nb077AlphaDummy238 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy237 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy238 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0234 (F I : SemanticCore.Class) : nb077AlphaDummy235 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy235 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy235 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0236 (F I : SemanticCore.Class) : nb077AlphaDummy140 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy141 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy140 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0237 (F I : SemanticCore.Class) : nb077AlphaDummy140 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy219 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy220 F I) (SemanticCore.Class.cv (nb077AlphaDummy141 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy219 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy219 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy220 F I) (SemanticCore.Class.cv (nb077AlphaDummy140 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy219 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0238 (x : SemanticCore.Var) : nb077AlphaDummy143 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy144 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy143 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0239 (x : SemanticCore.Var) : nb077AlphaDummy143 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy221 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy222 x) (SemanticCore.Class.cv (nb077AlphaDummy144 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy221 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy221 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy222 x) (SemanticCore.Class.cv (nb077AlphaDummy143 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy221 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0240 (F I : SemanticCore.Class) : nb077AlphaDummy140 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy219 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy220 F I) (SemanticCore.Class.cv (nb077AlphaDummy140 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy219 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy219 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy220 F I) (SemanticCore.Class.cv (nb077AlphaDummy140 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy219 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0241 (x : SemanticCore.Var) : nb077AlphaDummy143 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy221 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy222 x) (SemanticCore.Class.cv (nb077AlphaDummy143 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy221 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy221 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy222 x) (SemanticCore.Class.cv (nb077AlphaDummy143 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy221 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0242 (F I : SemanticCore.Class) : nb077AlphaDummy220 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0244 (F I : SemanticCore.Class) : nb077AlphaDummy220 F I ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy220 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0245 (x : SemanticCore.Var) : nb077AlphaDummy222 x ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy222 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0246 (F I : SemanticCore.Class) : nb077AlphaDummy000 F I ∈ {nb077AlphaDummy000 F I} ∪ {nb077AlphaDummy255 F I} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy255 F I)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0247 (x : SemanticCore.Var) : x ∈ {x} ∪ {nb077AlphaDummy256 x} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy256 x)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0248 (F I : SemanticCore.Class) : nb077AlphaDummy255 F I ∈ {nb077AlphaDummy000 F I} ∪ {nb077AlphaDummy255 F I} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy255 F I)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0249 (x : SemanticCore.Var) : nb077AlphaDummy256 x ∈ {x} ∪ {nb077AlphaDummy256 x} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy256 x)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0250 (F I : SemanticCore.Class) : nb077AlphaDummy000 F I ∈ {nb077AlphaDummy000 F I} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0251 (x : SemanticCore.Var) : x ∈ {x} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0252 (F I : SemanticCore.Class) : nb077AlphaDummy000 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy000 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy255 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0253 (F I : SemanticCore.Class) : nb077AlphaDummy000 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy259 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy260 F I) (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy259 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy259 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy260 F I) (SemanticCore.Class.cv (nb077AlphaDummy255 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy259 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0255 (x : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy261 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy262 x) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy261 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy261 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy262 x) (SemanticCore.Class.cv (nb077AlphaDummy256 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy261 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0256 (F I : SemanticCore.Class) : nb077AlphaDummy000 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy259 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy260 F I) (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy259 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy259 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy260 F I) (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy259 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0257 (x : SemanticCore.Var) : x ∈ (SemanticCore.Class.cab (nb077AlphaDummy261 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy262 x) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy261 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy261 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy262 x) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy261 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0258 (F I : SemanticCore.Class) : nb077AlphaDummy260 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy260 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0259 (x : SemanticCore.Var) : nb077AlphaDummy262 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy262 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0260 (F I : SemanticCore.Class) : nb077AlphaDummy267 F I ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy267 F I)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy267 F I)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy267 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0262 (F I : SemanticCore.Class) : nb077AlphaDummy267 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy267 F I)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0263 (x : SemanticCore.Var) : nb077AlphaDummy269 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy269 x)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0264 (F I : SemanticCore.Class) : nb077AlphaDummy274 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy274 F I)) (SemanticCore.Class.cv (nb077AlphaDummy275 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy274 F I)) (SemanticCore.Class.cv (nb077AlphaDummy275 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0265 (x : SemanticCore.Var) : nb077AlphaDummy277 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy277 x)) (SemanticCore.Class.cv (nb077AlphaDummy278 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy277 x)) (SemanticCore.Class.cv (nb077AlphaDummy278 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0266 (F I : SemanticCore.Class) : nb077AlphaDummy274 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy274 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy275 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0267 (x : SemanticCore.Var) : nb077AlphaDummy277 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy277 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy278 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0268 (F I : SemanticCore.Class) : nb077AlphaDummy275 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy274 F I)) (SemanticCore.Class.cv (nb077AlphaDummy275 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy274 F I)) (SemanticCore.Class.cv (nb077AlphaDummy275 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0269 (x : SemanticCore.Var) : nb077AlphaDummy278 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy277 x)) (SemanticCore.Class.cv (nb077AlphaDummy278 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy277 x)) (SemanticCore.Class.cv (nb077AlphaDummy278 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0270 (F I : SemanticCore.Class) : nb077AlphaDummy275 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy274 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy275 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0271 (x : SemanticCore.Var) : nb077AlphaDummy278 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy277 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy278 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0272 (F I : SemanticCore.Class) : nb077AlphaDummy274 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy274 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy275 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0273 (x : SemanticCore.Var) : nb077AlphaDummy277 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy277 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy278 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0274 (F I : SemanticCore.Class) : nb077AlphaDummy274 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy274 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy274 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0276 (F I : SemanticCore.Class) : nb077AlphaDummy275 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy274 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy275 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0277 (x : SemanticCore.Var) : nb077AlphaDummy278 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy277 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy278 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0278 (F I : SemanticCore.Class) : nb077AlphaDummy275 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy275 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy275 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0280 (F I : SemanticCore.Class) : nb077AlphaDummy255 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy000 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy255 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0281 (F I : SemanticCore.Class) : nb077AlphaDummy255 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy259 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy260 F I) (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy259 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy259 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy260 F I) (SemanticCore.Class.cv (nb077AlphaDummy255 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy259 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0283 (x : SemanticCore.Var) : nb077AlphaDummy256 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy261 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy262 x) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy261 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy261 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy262 x) (SemanticCore.Class.cv (nb077AlphaDummy256 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy261 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0284 (F I : SemanticCore.Class) : nb077AlphaDummy255 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy259 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy260 F I) (SemanticCore.Class.cv (nb077AlphaDummy255 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy259 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy259 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy260 F I) (SemanticCore.Class.cv (nb077AlphaDummy255 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy259 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0285 (x : SemanticCore.Var) : nb077AlphaDummy256 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy261 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy262 x) (SemanticCore.Class.cv (nb077AlphaDummy256 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy261 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy261 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy262 x) (SemanticCore.Class.cv (nb077AlphaDummy256 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy261 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0286 (F I : SemanticCore.Class) : nb077AlphaDummy260 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0288 (F I : SemanticCore.Class) : nb077AlphaDummy260 F I ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy260 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0289 (x : SemanticCore.Var) : nb077AlphaDummy262 x ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy262 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0290 (F I : SemanticCore.Class) : nb077AlphaDummy000 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy000 F I)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0292 (F I : SemanticCore.Class) : nb077AlphaDummy296 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy296 F I)) (SemanticCore.Class.cv (nb077AlphaDummy297 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy296 F I)) (SemanticCore.Class.cv (nb077AlphaDummy297 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0293 (x : SemanticCore.Var) : nb077AlphaDummy299 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy299 x)) (SemanticCore.Class.cv (nb077AlphaDummy300 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy299 x)) (SemanticCore.Class.cv (nb077AlphaDummy300 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0294 (F I : SemanticCore.Class) : nb077AlphaDummy296 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy296 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy297 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0295 (x : SemanticCore.Var) : nb077AlphaDummy299 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy299 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy300 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0296 (F I : SemanticCore.Class) : nb077AlphaDummy297 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy296 F I)) (SemanticCore.Class.cv (nb077AlphaDummy297 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy296 F I)) (SemanticCore.Class.cv (nb077AlphaDummy297 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0297 (x : SemanticCore.Var) : nb077AlphaDummy300 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy299 x)) (SemanticCore.Class.cv (nb077AlphaDummy300 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy299 x)) (SemanticCore.Class.cv (nb077AlphaDummy300 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0298 (F I : SemanticCore.Class) : nb077AlphaDummy297 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy296 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy297 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0299 (x : SemanticCore.Var) : nb077AlphaDummy300 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy299 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy300 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0300 (F I : SemanticCore.Class) : nb077AlphaDummy296 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy296 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy297 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0301 (x : SemanticCore.Var) : nb077AlphaDummy299 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy299 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy300 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0302 (F I : SemanticCore.Class) : nb077AlphaDummy296 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy296 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy296 F I)).fv

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