Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C068C001Block002

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C068C001Part006.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_192 (f : SemanticCore.Var) :

nb068AlphaDummy160 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy150 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy150 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_193 :

nb068AlphaDummy175 ∉ (SemanticCore.Class.cv nb068AlphaDummy168).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_194 :

nb068AlphaDummy176 ∉ (SemanticCore.Class.cv nb068AlphaDummy168).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_195 :

nb068AlphaDummy175 ≠ nb068AlphaDummy176

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_196 (f : SemanticCore.Var) :

nb068AlphaDummy177 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy170 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_197 (f : SemanticCore.Var) :

nb068AlphaDummy178 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy170 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_198 (f : SemanticCore.Var) :

nb068AlphaDummy177 f ≠ nb068AlphaDummy178 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_199 :

nb068AlphaDummy181 ∉ (SemanticCore.Class.cv nb068AlphaDummy175).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_200 :

nb068AlphaDummy182 ∉ (SemanticCore.Class.cv nb068AlphaDummy175).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_201 :

nb068AlphaDummy183 ∉ (SemanticCore.Class.cv nb068AlphaDummy175).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_202 :

nb068AlphaDummy181 ≠ nb068AlphaDummy182

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_203 :

nb068AlphaDummy181 ≠ nb068AlphaDummy183

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_204 :

nb068AlphaDummy182 ≠ nb068AlphaDummy183

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_205 (f : SemanticCore.Var) :

nb068AlphaDummy184 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy177 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_206 (f : SemanticCore.Var) :

nb068AlphaDummy185 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy177 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_207 (f : SemanticCore.Var) :

nb068AlphaDummy186 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy177 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_208 (f : SemanticCore.Var) :

nb068AlphaDummy184 f ≠ nb068AlphaDummy185 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_209 (f : SemanticCore.Var) :

nb068AlphaDummy184 f ≠ nb068AlphaDummy186 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_210 (f : SemanticCore.Var) :

nb068AlphaDummy185 f ≠ nb068AlphaDummy186 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_211 :

nb068AlphaDummy193 ∉ (SemanticCore.Class.cv nb068AlphaDummy182).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy182).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_212 :

nb068AlphaDummy189 ∉ (SemanticCore.Class.cv nb068AlphaDummy182).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy183).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_213 :

nb068AlphaDummy195 ∉ (SemanticCore.Class.cv nb068AlphaDummy183).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy183).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_214 (f : SemanticCore.Var) :

nb068AlphaDummy194 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy185 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy185 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_215 (f : SemanticCore.Var) :

nb068AlphaDummy190 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy185 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy186 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_216 (f : SemanticCore.Var) :

nb068AlphaDummy196 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy186 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy186 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_217 :

nb068AlphaDummy211 ∉ (SemanticCore.Class.cv nb068AlphaDummy204).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_218 :

nb068AlphaDummy212 ∉ (SemanticCore.Class.cv nb068AlphaDummy204).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_219 :

nb068AlphaDummy211 ≠ nb068AlphaDummy212

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_220 (f : SemanticCore.Var) :

nb068AlphaDummy213 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy206 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_221 (f : SemanticCore.Var) :

nb068AlphaDummy214 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy206 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_222 (f : SemanticCore.Var) :

nb068AlphaDummy213 f ≠ nb068AlphaDummy214 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_223 :

nb068AlphaDummy217 ∉ (SemanticCore.Class.cv nb068AlphaDummy211).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_224 :

nb068AlphaDummy218 ∉ (SemanticCore.Class.cv nb068AlphaDummy211).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_225 :

nb068AlphaDummy219 ∉ (SemanticCore.Class.cv nb068AlphaDummy211).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_226 :

nb068AlphaDummy217 ≠ nb068AlphaDummy218

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_227 :

nb068AlphaDummy217 ≠ nb068AlphaDummy219

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_228 :

nb068AlphaDummy218 ≠ nb068AlphaDummy219

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_229 (f : SemanticCore.Var) :

nb068AlphaDummy220 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy213 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_230 (f : SemanticCore.Var) :

nb068AlphaDummy221 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy213 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_231 (f : SemanticCore.Var) :

nb068AlphaDummy222 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy213 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_232 (f : SemanticCore.Var) :

nb068AlphaDummy220 f ≠ nb068AlphaDummy221 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_233 (f : SemanticCore.Var) :

nb068AlphaDummy220 f ≠ nb068AlphaDummy222 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_234 (f : SemanticCore.Var) :

nb068AlphaDummy221 f ≠ nb068AlphaDummy222 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_235 :

nb068AlphaDummy229 ∉ (SemanticCore.Class.cv nb068AlphaDummy218).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy218).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_236 :

nb068AlphaDummy225 ∉ (SemanticCore.Class.cv nb068AlphaDummy218).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy219).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_237 :

nb068AlphaDummy231 ∉ (SemanticCore.Class.cv nb068AlphaDummy219).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy219).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_238 (f : SemanticCore.Var) :

nb068AlphaDummy230 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy221 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy221 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_239 (f : SemanticCore.Var) :

nb068AlphaDummy226 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy221 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy222 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_240 (f : SemanticCore.Var) :

nb068AlphaDummy232 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy222 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy222 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_241 :

nb068AlphaDummy243 ∉ (SemanticCore.Class.cv nb068AlphaDummy240).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy239).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_242 :

nb068AlphaDummy244 ∉ (SemanticCore.Class.cv nb068AlphaDummy240).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy239).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_243 :

nb068AlphaDummy243 ≠ nb068AlphaDummy244

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_244 (f : SemanticCore.Var) :

nb068AlphaDummy245 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy242 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy241 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_245 (f : SemanticCore.Var) :

nb068AlphaDummy246 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy242 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy241 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_246 (f : SemanticCore.Var) :

nb068AlphaDummy245 f ≠ nb068AlphaDummy246 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_247 :

nb068AlphaDummy251 ∉ (SemanticCore.Class.cv nb068AlphaDummy244).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_248 :

nb068AlphaDummy252 ∉ (SemanticCore.Class.cv nb068AlphaDummy244).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_249 :

nb068AlphaDummy251 ≠ nb068AlphaDummy252

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_250 (f : SemanticCore.Var) :

nb068AlphaDummy253 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy246 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_251 (f : SemanticCore.Var) :

nb068AlphaDummy254 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy246 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_252 (f : SemanticCore.Var) :

nb068AlphaDummy253 f ≠ nb068AlphaDummy254 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_253 :

nb068AlphaDummy257 ∉ (SemanticCore.Class.cv nb068AlphaDummy251).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_254 :

nb068AlphaDummy258 ∉ (SemanticCore.Class.cv nb068AlphaDummy251).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_255 :

nb068AlphaDummy259 ∉ (SemanticCore.Class.cv nb068AlphaDummy251).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_256 :

nb068AlphaDummy257 ≠ nb068AlphaDummy258

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_257 :

nb068AlphaDummy257 ≠ nb068AlphaDummy259

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_258 :

nb068AlphaDummy258 ≠ nb068AlphaDummy259

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_259 (f : SemanticCore.Var) :

nb068AlphaDummy260 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy253 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_260 (f : SemanticCore.Var) :

nb068AlphaDummy261 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy253 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_261 (f : SemanticCore.Var) :

nb068AlphaDummy262 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy253 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_262 (f : SemanticCore.Var) :

nb068AlphaDummy260 f ≠ nb068AlphaDummy261 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_263 (f : SemanticCore.Var) :

nb068AlphaDummy260 f ≠ nb068AlphaDummy262 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_264 (f : SemanticCore.Var) :

nb068AlphaDummy261 f ≠ nb068AlphaDummy262 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_265 :

nb068AlphaDummy269 ∉ (SemanticCore.Class.cv nb068AlphaDummy258).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy258).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_266 :

nb068AlphaDummy265 ∉ (SemanticCore.Class.cv nb068AlphaDummy258).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy259).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_267 :

nb068AlphaDummy271 ∉ (SemanticCore.Class.cv nb068AlphaDummy259).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy259).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_268 (f : SemanticCore.Var) :

nb068AlphaDummy270 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy261 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy261 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_269 (f : SemanticCore.Var) :

nb068AlphaDummy266 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy261 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy262 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_270 (f : SemanticCore.Var) :

nb068AlphaDummy272 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy262 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy262 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_271 :

nb068AlphaDummy287 ∉ (SemanticCore.Class.cv nb068AlphaDummy284).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy283).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_272 :

nb068AlphaDummy288 ∉ (SemanticCore.Class.cv nb068AlphaDummy284).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy283).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_273 :

nb068AlphaDummy287 ≠ nb068AlphaDummy288

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_274 (f : SemanticCore.Var) :

nb068AlphaDummy289 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy286 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy285 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_275 (f : SemanticCore.Var) :

nb068AlphaDummy290 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy286 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy285 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_276 (f : SemanticCore.Var) :

nb068AlphaDummy289 f ≠ nb068AlphaDummy290 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_277 :

nb068AlphaDummy295 ∉ (SemanticCore.Class.cv nb068AlphaDummy288).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_278 :

nb068AlphaDummy296 ∉ (SemanticCore.Class.cv nb068AlphaDummy288).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_279 :

nb068AlphaDummy295 ≠ nb068AlphaDummy296

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_280 (f : SemanticCore.Var) :

nb068AlphaDummy297 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy290 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_281 (f : SemanticCore.Var) :

nb068AlphaDummy298 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy290 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_282 (f : SemanticCore.Var) :

nb068AlphaDummy297 f ≠ nb068AlphaDummy298 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_283 :

nb068AlphaDummy301 ∉ (SemanticCore.Class.cv nb068AlphaDummy295).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_284 :

nb068AlphaDummy302 ∉ (SemanticCore.Class.cv nb068AlphaDummy295).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_285 :

nb068AlphaDummy303 ∉ (SemanticCore.Class.cv nb068AlphaDummy295).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_286 :

nb068AlphaDummy301 ≠ nb068AlphaDummy302

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_287 :

nb068AlphaDummy301 ≠ nb068AlphaDummy303

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_288 :

nb068AlphaDummy302 ≠ nb068AlphaDummy303

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_289 (f : SemanticCore.Var) :

nb068AlphaDummy304 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy297 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_290 (f : SemanticCore.Var) :

nb068AlphaDummy305 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy297 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_291 (f : SemanticCore.Var) :

nb068AlphaDummy306 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy297 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_292 (f : SemanticCore.Var) :

nb068AlphaDummy304 f ≠ nb068AlphaDummy305 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_293 (f : SemanticCore.Var) :

nb068AlphaDummy304 f ≠ nb068AlphaDummy306 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_294 (f : SemanticCore.Var) :

nb068AlphaDummy305 f ≠ nb068AlphaDummy306 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_295 :

nb068AlphaDummy313 ∉ (SemanticCore.Class.cv nb068AlphaDummy302).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy302).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_296 :

nb068AlphaDummy309 ∉ (SemanticCore.Class.cv nb068AlphaDummy302).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy303).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_297 :

nb068AlphaDummy315 ∉ (SemanticCore.Class.cv nb068AlphaDummy303).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy303).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_298 (f : SemanticCore.Var) :

nb068AlphaDummy314 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy305 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy305 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_299 (f : SemanticCore.Var) :

nb068AlphaDummy310 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy305 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy306 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_300 (f : SemanticCore.Var) :

nb068AlphaDummy316 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy306 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy306 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_301 :

nb068AlphaDummy335 ∉ (SemanticCore.Class.cv nb068AlphaDummy327).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy328).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_302 :

nb068AlphaDummy336 ∉ (SemanticCore.Class.cv nb068AlphaDummy327).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy328).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_303 :

nb068AlphaDummy335 ≠ nb068AlphaDummy336

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_304 :

nb068AlphaDummy371 ∉ (SemanticCore.Class.cv nb068AlphaDummy327).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy329).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_305 :

nb068AlphaDummy372 ∉ (SemanticCore.Class.cv nb068AlphaDummy327).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy329).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_306 :

nb068AlphaDummy371 ≠ nb068AlphaDummy372

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_307 :

nb068AlphaDummy485 ∉ (SemanticCore.Class.cv nb068AlphaDummy329).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy328).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_308 :

nb068AlphaDummy486 ∉ (SemanticCore.Class.cv nb068AlphaDummy329).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy328).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_309 :

nb068AlphaDummy485 ≠ nb068AlphaDummy486

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_310 (f : SemanticCore.Var) :

nb068AlphaDummy337 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy330 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy331 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_311 (f : SemanticCore.Var) :

nb068AlphaDummy338 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy330 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy331 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_312 (f : SemanticCore.Var) :

nb068AlphaDummy337 f ≠ nb068AlphaDummy338 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_313 (f : SemanticCore.Var) :

nb068AlphaDummy373 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy330 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy332 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_314 (f : SemanticCore.Var) :

nb068AlphaDummy374 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy330 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy332 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_315 (f : SemanticCore.Var) :

nb068AlphaDummy373 f ≠ nb068AlphaDummy374 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_316 (f : SemanticCore.Var) :

nb068AlphaDummy487 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy332 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy331 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_317 (f : SemanticCore.Var) :

nb068AlphaDummy488 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy332 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy331 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_318 (f : SemanticCore.Var) :

nb068AlphaDummy487 f ≠ nb068AlphaDummy488 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_319 :

nb068AlphaDummy343 ∉ (SemanticCore.Class.cv nb068AlphaDummy336).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_320 :

nb068AlphaDummy344 ∉ (SemanticCore.Class.cv nb068AlphaDummy336).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_321 :

nb068AlphaDummy343 ≠ nb068AlphaDummy344

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_322 (f : SemanticCore.Var) :

nb068AlphaDummy345 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy338 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_323 (f : SemanticCore.Var) :

nb068AlphaDummy346 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy338 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_324 (f : SemanticCore.Var) :

nb068AlphaDummy345 f ≠ nb068AlphaDummy346 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_325 :

nb068AlphaDummy349 ∉ (SemanticCore.Class.cv nb068AlphaDummy343).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_326 :

nb068AlphaDummy350 ∉ (SemanticCore.Class.cv nb068AlphaDummy343).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_327 :

nb068AlphaDummy351 ∉ (SemanticCore.Class.cv nb068AlphaDummy343).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_328 :

nb068AlphaDummy349 ≠ nb068AlphaDummy350

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_329 :

nb068AlphaDummy349 ≠ nb068AlphaDummy351

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_330 :

nb068AlphaDummy350 ≠ nb068AlphaDummy351

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_331 (f : SemanticCore.Var) :

nb068AlphaDummy352 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy345 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_332 (f : SemanticCore.Var) :

nb068AlphaDummy353 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy345 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_333 (f : SemanticCore.Var) :

nb068AlphaDummy354 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy345 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_334 (f : SemanticCore.Var) :

nb068AlphaDummy352 f ≠ nb068AlphaDummy353 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_335 (f : SemanticCore.Var) :

nb068AlphaDummy352 f ≠ nb068AlphaDummy354 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_336 (f : SemanticCore.Var) :

nb068AlphaDummy353 f ≠ nb068AlphaDummy354 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_337 :

nb068AlphaDummy361 ∉ (SemanticCore.Class.cv nb068AlphaDummy350).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy350).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_338 :

nb068AlphaDummy357 ∉ (SemanticCore.Class.cv nb068AlphaDummy350).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy351).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_339 :

nb068AlphaDummy363 ∉ (SemanticCore.Class.cv nb068AlphaDummy351).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy351).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_340 (f : SemanticCore.Var) :

nb068AlphaDummy362 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy353 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy353 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_341 (f : SemanticCore.Var) :

nb068AlphaDummy358 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy353 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy354 f)).fv

Certificates from NAR4C068C001Part007.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_342 (f : SemanticCore.Var) :

nb068AlphaDummy364 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy354 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy354 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_343 :

nb068AlphaDummy379 ∉ (SemanticCore.Class.cv nb068AlphaDummy372).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_344 :

nb068AlphaDummy380 ∉ (SemanticCore.Class.cv nb068AlphaDummy372).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_345 :

nb068AlphaDummy379 ≠ nb068AlphaDummy380

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_346 (f : SemanticCore.Var) :

nb068AlphaDummy381 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy374 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_347 (f : SemanticCore.Var) :

nb068AlphaDummy382 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy374 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_348 (f : SemanticCore.Var) :

nb068AlphaDummy381 f ≠ nb068AlphaDummy382 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_349 :

nb068AlphaDummy385 ∉ (SemanticCore.Class.cv nb068AlphaDummy379).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_350 :

nb068AlphaDummy386 ∉ (SemanticCore.Class.cv nb068AlphaDummy379).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_351 :

nb068AlphaDummy387 ∉ (SemanticCore.Class.cv nb068AlphaDummy379).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_352 :

nb068AlphaDummy385 ≠ nb068AlphaDummy386

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_353 :

nb068AlphaDummy385 ≠ nb068AlphaDummy387

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_354 :

nb068AlphaDummy386 ≠ nb068AlphaDummy387

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_355 (f : SemanticCore.Var) :

nb068AlphaDummy388 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy381 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_356 (f : SemanticCore.Var) :

nb068AlphaDummy389 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy381 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_357 (f : SemanticCore.Var) :

nb068AlphaDummy390 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy381 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_358 (f : SemanticCore.Var) :

nb068AlphaDummy388 f ≠ nb068AlphaDummy389 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_359 (f : SemanticCore.Var) :

nb068AlphaDummy388 f ≠ nb068AlphaDummy390 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_360 (f : SemanticCore.Var) :

nb068AlphaDummy389 f ≠ nb068AlphaDummy390 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_361 :

nb068AlphaDummy397 ∉ (SemanticCore.Class.cv nb068AlphaDummy386).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy386).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_362 :

nb068AlphaDummy393 ∉ (SemanticCore.Class.cv nb068AlphaDummy386).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy387).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_363 :

nb068AlphaDummy399 ∉ (SemanticCore.Class.cv nb068AlphaDummy387).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy387).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_364 (f : SemanticCore.Var) :

nb068AlphaDummy398 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy389 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy389 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_365 (f : SemanticCore.Var) :

nb068AlphaDummy394 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy389 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy390 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_366 (f : SemanticCore.Var) :

nb068AlphaDummy400 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy390 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy390 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_367 :

nb068AlphaDummy413 ∉ (SemanticCore.Class.cv nb068AlphaDummy407).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy408).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_368 :

nb068AlphaDummy414 ∉ (SemanticCore.Class.cv nb068AlphaDummy407).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy408).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_369 :

nb068AlphaDummy413 ≠ nb068AlphaDummy414

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_370 :

nb068AlphaDummy449 ∉ (SemanticCore.Class.cv nb068AlphaDummy408).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy407).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_371 :

nb068AlphaDummy450 ∉ (SemanticCore.Class.cv nb068AlphaDummy408).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy407).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_372 :

nb068AlphaDummy449 ≠ nb068AlphaDummy450

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_373 (f : SemanticCore.Var) :

nb068AlphaDummy415 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy409 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy410 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_374 (f : SemanticCore.Var) :

nb068AlphaDummy416 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy409 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy410 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_375 (f : SemanticCore.Var) :

nb068AlphaDummy415 f ≠ nb068AlphaDummy416 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_376 (f : SemanticCore.Var) :

nb068AlphaDummy451 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy410 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy409 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_377 (f : SemanticCore.Var) :

nb068AlphaDummy452 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy410 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy409 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_378 (f : SemanticCore.Var) :

nb068AlphaDummy451 f ≠ nb068AlphaDummy452 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_379 :

nb068AlphaDummy421 ∉ (SemanticCore.Class.cv nb068AlphaDummy414).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_380 :

nb068AlphaDummy422 ∉ (SemanticCore.Class.cv nb068AlphaDummy414).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_381 :

nb068AlphaDummy421 ≠ nb068AlphaDummy422

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_382 (f : SemanticCore.Var) :

nb068AlphaDummy423 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy416 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_383 (f : SemanticCore.Var) :

nb068AlphaDummy424 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy416 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_384 (f : SemanticCore.Var) :

nb068AlphaDummy423 f ≠ nb068AlphaDummy424 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_385 :

nb068AlphaDummy427 ∉ (SemanticCore.Class.cv nb068AlphaDummy421).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_386 :

nb068AlphaDummy428 ∉ (SemanticCore.Class.cv nb068AlphaDummy421).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_387 :

nb068AlphaDummy429 ∉ (SemanticCore.Class.cv nb068AlphaDummy421).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_388 :

nb068AlphaDummy427 ≠ nb068AlphaDummy428

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_389 :

nb068AlphaDummy427 ≠ nb068AlphaDummy429

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_390 :

nb068AlphaDummy428 ≠ nb068AlphaDummy429

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_391 (f : SemanticCore.Var) :

nb068AlphaDummy430 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy423 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_392 (f : SemanticCore.Var) :

nb068AlphaDummy431 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy423 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_393 (f : SemanticCore.Var) :

nb068AlphaDummy432 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy423 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_394 (f : SemanticCore.Var) :

nb068AlphaDummy430 f ≠ nb068AlphaDummy431 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_395 (f : SemanticCore.Var) :

nb068AlphaDummy430 f ≠ nb068AlphaDummy432 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_396 (f : SemanticCore.Var) :

nb068AlphaDummy431 f ≠ nb068AlphaDummy432 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_397 :

nb068AlphaDummy439 ∉ (SemanticCore.Class.cv nb068AlphaDummy428).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy428).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_398 :

nb068AlphaDummy435 ∉ (SemanticCore.Class.cv nb068AlphaDummy428).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy429).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_399 :

nb068AlphaDummy441 ∉ (SemanticCore.Class.cv nb068AlphaDummy429).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy429).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_400 (f : SemanticCore.Var) :

nb068AlphaDummy440 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy431 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy431 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_401 (f : SemanticCore.Var) :

nb068AlphaDummy436 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy431 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy432 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_402 (f : SemanticCore.Var) :

nb068AlphaDummy442 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy432 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy432 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_403 :

nb068AlphaDummy457 ∉ (SemanticCore.Class.cv nb068AlphaDummy450).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_404 :

nb068AlphaDummy458 ∉ (SemanticCore.Class.cv nb068AlphaDummy450).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_405 :

nb068AlphaDummy457 ≠ nb068AlphaDummy458

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_406 (f : SemanticCore.Var) :

nb068AlphaDummy459 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy452 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_407 (f : SemanticCore.Var) :

nb068AlphaDummy460 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy452 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_408 (f : SemanticCore.Var) :

nb068AlphaDummy459 f ≠ nb068AlphaDummy460 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_409 :

nb068AlphaDummy463 ∉ (SemanticCore.Class.cv nb068AlphaDummy457).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_410 :

nb068AlphaDummy464 ∉ (SemanticCore.Class.cv nb068AlphaDummy457).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_411 :

nb068AlphaDummy465 ∉ (SemanticCore.Class.cv nb068AlphaDummy457).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_412 :

nb068AlphaDummy463 ≠ nb068AlphaDummy464

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_413 :

nb068AlphaDummy463 ≠ nb068AlphaDummy465

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_414 :

nb068AlphaDummy464 ≠ nb068AlphaDummy465

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_415 (f : SemanticCore.Var) :

nb068AlphaDummy466 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy459 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_416 (f : SemanticCore.Var) :

nb068AlphaDummy467 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy459 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_417 (f : SemanticCore.Var) :

nb068AlphaDummy468 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy459 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_418 (f : SemanticCore.Var) :

nb068AlphaDummy466 f ≠ nb068AlphaDummy467 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_419 (f : SemanticCore.Var) :

nb068AlphaDummy466 f ≠ nb068AlphaDummy468 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_420 (f : SemanticCore.Var) :

nb068AlphaDummy467 f ≠ nb068AlphaDummy468 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_421 :

nb068AlphaDummy475 ∉ (SemanticCore.Class.cv nb068AlphaDummy464).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy464).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_422 :

nb068AlphaDummy471 ∉ (SemanticCore.Class.cv nb068AlphaDummy464).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy465).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_423 :

nb068AlphaDummy477 ∉ (SemanticCore.Class.cv nb068AlphaDummy465).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy465).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_424 (f : SemanticCore.Var) :

nb068AlphaDummy476 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy467 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy467 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_425 (f : SemanticCore.Var) :

nb068AlphaDummy472 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy467 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy468 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_426 (f : SemanticCore.Var) :

nb068AlphaDummy478 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy468 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy468 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_427 :

nb068AlphaDummy493 ∉ (SemanticCore.Class.cv nb068AlphaDummy486).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_428 :

nb068AlphaDummy494 ∉ (SemanticCore.Class.cv nb068AlphaDummy486).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_429 :

nb068AlphaDummy493 ≠ nb068AlphaDummy494

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_430 (f : SemanticCore.Var) :

nb068AlphaDummy495 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy488 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_431 (f : SemanticCore.Var) :

nb068AlphaDummy496 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy488 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_432 (f : SemanticCore.Var) :

nb068AlphaDummy495 f ≠ nb068AlphaDummy496 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_433 :

nb068AlphaDummy499 ∉ (SemanticCore.Class.cv nb068AlphaDummy493).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_434 :

nb068AlphaDummy500 ∉ (SemanticCore.Class.cv nb068AlphaDummy493).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_435 :

nb068AlphaDummy501 ∉ (SemanticCore.Class.cv nb068AlphaDummy493).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_436 :

nb068AlphaDummy499 ≠ nb068AlphaDummy500

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_437 :

nb068AlphaDummy499 ≠ nb068AlphaDummy501

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_438 :

nb068AlphaDummy500 ≠ nb068AlphaDummy501

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_439 (f : SemanticCore.Var) :

nb068AlphaDummy502 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy495 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_440 (f : SemanticCore.Var) :

nb068AlphaDummy503 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy495 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_441 (f : SemanticCore.Var) :

nb068AlphaDummy504 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy495 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_442 (f : SemanticCore.Var) :

nb068AlphaDummy502 f ≠ nb068AlphaDummy503 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_443 (f : SemanticCore.Var) :

nb068AlphaDummy502 f ≠ nb068AlphaDummy504 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_444 (f : SemanticCore.Var) :

nb068AlphaDummy503 f ≠ nb068AlphaDummy504 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_445 :

nb068AlphaDummy511 ∉ (SemanticCore.Class.cv nb068AlphaDummy500).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy500).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_446 :

nb068AlphaDummy507 ∉ (SemanticCore.Class.cv nb068AlphaDummy500).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy501).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_447 :

nb068AlphaDummy513 ∉ (SemanticCore.Class.cv nb068AlphaDummy501).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy501).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_448 (f : SemanticCore.Var) :

nb068AlphaDummy512 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy503 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy503 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_449 (f : SemanticCore.Var) :

nb068AlphaDummy508 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy503 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy504 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_450 (f : SemanticCore.Var) :

nb068AlphaDummy514 f ∉ (SemanticCore.Class.cv (nb068AlphaDummy504 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy504 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_451 (f : SemanticCore.Var) :

nb068AlphaDummy127 f ∉ (SemanticCore.Class.cv f).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_452 (f : SemanticCore.Var) :

nb068AlphaDummy128 f ∉ (SemanticCore.Class.cv f).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_453 (f : SemanticCore.Var) :

nb068AlphaDummy127 f ≠ nb068AlphaDummy128 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_454 (f : SemanticCore.Var) :

nb068AlphaDummy048 f ∉ (SemanticCore.Class.cv f).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_455 (f : SemanticCore.Var) :

nb068AlphaDummy049 f ∉ (SemanticCore.Class.cv f).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_456 (f : SemanticCore.Var) :

nb068AlphaDummy050 f ∉ (SemanticCore.Class.cv f).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_457 (f : SemanticCore.Var) :

nb068AlphaDummy048 f ≠ nb068AlphaDummy049 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_458 (f : SemanticCore.Var) :

nb068AlphaDummy048 f ≠ nb068AlphaDummy050 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_459 (f : SemanticCore.Var) :

nb068AlphaDummy049 f ≠ nb068AlphaDummy050 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_460 (f : SemanticCore.Var) :

nb068AlphaDummy285 f ∉ (SemanticCore.Class.cv f).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_461 (f : SemanticCore.Var) :

nb068AlphaDummy286 f ∉ (SemanticCore.Class.cv f).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_462 (f : SemanticCore.Var) :

nb068AlphaDummy285 f ≠ nb068AlphaDummy286 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_463 (x y : SemanticCore.Var) :

nb068AlphaDummy007 x y ∉ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_464 (x y : SemanticCore.Var) :

nb068AlphaDummy008 x y ∉ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_465 (x y : SemanticCore.Var) :

nb068AlphaDummy007 x y ≠ nb068AlphaDummy008 x y

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_466 :

nb068AlphaDummy017 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy013) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy013) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy013).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_467 (x y : SemanticCore.Var) :

nb068AlphaDummy018 x y ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy015 x y)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy015 x y)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy015 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_468 :

nb068AlphaDummy065 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy061) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy061) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy061).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_469 (f : SemanticCore.Var) :

nb068AlphaDummy066 f ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy063 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy063 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy063 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_470 :

nb068AlphaDummy101 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy097) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy097) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy097).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_471 (f : SemanticCore.Var) :

nb068AlphaDummy102 f ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy099 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy099 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy099 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_472 :

nb068AlphaDummy143 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy139).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_473 (f : SemanticCore.Var) :

nb068AlphaDummy144 f ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy141 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_474 :

nb068AlphaDummy179 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy175).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_475 (f : SemanticCore.Var) :

nb068AlphaDummy180 f ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy177 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_476 :

nb068AlphaDummy215 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy211) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy211) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy211).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_477 (f : SemanticCore.Var) :

nb068AlphaDummy216 f ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy213 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy213 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy213 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_478 :

nb068AlphaDummy255 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy251) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy251) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy251).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_479 (f : SemanticCore.Var) :

nb068AlphaDummy256 f ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy253 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy253 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy253 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_480 :

nb068AlphaDummy299 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy295) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy295) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy295).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_481 (f : SemanticCore.Var) :

nb068AlphaDummy300 f ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy297 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy297 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy297 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_482 :

nb068AlphaDummy347 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy343) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy343) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy343).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_483 (f : SemanticCore.Var) :

nb068AlphaDummy348 f ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy345 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy345 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy345 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_484 :

nb068AlphaDummy383 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy379) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy379) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy379).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_485 (f : SemanticCore.Var) :

nb068AlphaDummy384 f ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy381 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy381 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy381 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_486 :

nb068AlphaDummy425 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy421) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy421) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy421).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_487 (f : SemanticCore.Var) :

nb068AlphaDummy426 f ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy423 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy423 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy423 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_488 :

nb068AlphaDummy461 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy457) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy457) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy457).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_489 (f : SemanticCore.Var) :

nb068AlphaDummy462 f ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy459 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy459 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy459 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_490 :

nb068AlphaDummy497 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy493) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy493) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy493).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_491 (f : SemanticCore.Var) :

nb068AlphaDummy498 f ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy495 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy495 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy495 f)).fv

Certificates from NAR4C068C001Part008.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_492 :

nb068AlphaDummy407 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_493 :

nb068AlphaDummy408 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_494 :

nb068AlphaDummy407 ≠ nb068AlphaDummy408

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_495 :

nb068AlphaDummy327 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_496 :

nb068AlphaDummy328 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_497 :

nb068AlphaDummy329 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_498 :

nb068AlphaDummy327 ≠ nb068AlphaDummy328

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_499 :

nb068AlphaDummy327 ≠ nb068AlphaDummy329

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_500 :

nb068AlphaDummy328 ≠ nb068AlphaDummy329

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_501 :

nb068AlphaDummy239 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_502 :

nb068AlphaDummy240 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_503 :

nb068AlphaDummy239 ≠ nb068AlphaDummy240

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_504 (f : SemanticCore.Var) :

nb068AlphaDummy409 f ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_505 (f : SemanticCore.Var) :

nb068AlphaDummy410 f ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_506 (f : SemanticCore.Var) :

nb068AlphaDummy409 f ≠ nb068AlphaDummy410 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_507 (f : SemanticCore.Var) :

nb068AlphaDummy330 f ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_508 (f : SemanticCore.Var) :

nb068AlphaDummy331 f ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_509 (f : SemanticCore.Var) :

nb068AlphaDummy332 f ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_510 (f : SemanticCore.Var) :

nb068AlphaDummy330 f ≠ nb068AlphaDummy331 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_511 (f : SemanticCore.Var) :

nb068AlphaDummy330 f ≠ nb068AlphaDummy332 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_512 (f : SemanticCore.Var) :

nb068AlphaDummy331 f ≠ nb068AlphaDummy332 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_513 (f : SemanticCore.Var) :

nb068AlphaDummy241 f ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_514 (f : SemanticCore.Var) :

nb068AlphaDummy242 f ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_515 (f : SemanticCore.Var) :

nb068AlphaDummy241 f ≠ nb068AlphaDummy242 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_516 :

nb068AlphaDummy043 ∉ (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb068AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_517 (f : SemanticCore.Var) :

nb068AlphaDummy044 f ∉ (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_518 :

nb068AlphaDummy325 ∉ (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_519 (f : SemanticCore.Var) :

nb068AlphaDummy326 f ∉ (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_520 :

nb068AlphaDummy009 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy006 (SemanticCore.Class.cv nb068AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy005) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy006 (SemanticCore.Class.cv nb068AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_521 (x y : SemanticCore.Var) :

nb068AlphaDummy010 x y ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy008 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy008 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_522 :

nb068AlphaDummy057 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy054 (SemanticCore.Class.cv nb068AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy054 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_523 (f : SemanticCore.Var) :

nb068AlphaDummy058 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy056 f) (SemanticCore.Class.cv (nb068AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy056 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_524 :

nb068AlphaDummy093 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_525 (f : SemanticCore.Var) :

nb068AlphaDummy094 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_526 :

nb068AlphaDummy135 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_527 (f : SemanticCore.Var) :

nb068AlphaDummy136 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_528 :

nb068AlphaDummy171 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_529 (f : SemanticCore.Var) :

nb068AlphaDummy172 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_530 :

nb068AlphaDummy207 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy203 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy204 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy203 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy204 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_531 (f : SemanticCore.Var) :

nb068AlphaDummy208 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy205 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy206 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy205 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy206 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_532 :

nb068AlphaDummy247 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy243 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy244 (SemanticCore.Class.cv nb068AlphaDummy240) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy243 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy244 (SemanticCore.Class.cv nb068AlphaDummy239) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_533 (f : SemanticCore.Var) :

nb068AlphaDummy248 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy245 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy246 f) (SemanticCore.Class.cv (nb068AlphaDummy242 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy245 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy246 f) (SemanticCore.Class.cv (nb068AlphaDummy241 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_534 :

nb068AlphaDummy291 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy287 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy284) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy287 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy283) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_535 (f : SemanticCore.Var) :

nb068AlphaDummy292 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy289 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy286 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy289 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy285 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_536 :

nb068AlphaDummy339 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy335 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy336 (SemanticCore.Class.cv nb068AlphaDummy327) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy335 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy336 (SemanticCore.Class.cv nb068AlphaDummy328) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_537 (f : SemanticCore.Var) :

nb068AlphaDummy340 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy337 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy338 f) (SemanticCore.Class.cv (nb068AlphaDummy330 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy337 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy338 f) (SemanticCore.Class.cv (nb068AlphaDummy331 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_538 :

nb068AlphaDummy375 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy371 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy372 (SemanticCore.Class.cv nb068AlphaDummy327) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy371) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy371 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy372 (SemanticCore.Class.cv nb068AlphaDummy329) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy371) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_539 (f : SemanticCore.Var) :

nb068AlphaDummy376 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy373 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy374 f) (SemanticCore.Class.cv (nb068AlphaDummy330 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy373 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy373 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy374 f) (SemanticCore.Class.cv (nb068AlphaDummy332 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy373 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_540 :

nb068AlphaDummy417 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy413 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy414 (SemanticCore.Class.cv nb068AlphaDummy407) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy413) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy413 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy414 (SemanticCore.Class.cv nb068AlphaDummy408) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy413) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_541 (f : SemanticCore.Var) :

nb068AlphaDummy418 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy415 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy416 f) (SemanticCore.Class.cv (nb068AlphaDummy409 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy415 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy415 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy416 f) (SemanticCore.Class.cv (nb068AlphaDummy410 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy415 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_542 :

nb068AlphaDummy453 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy449 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy450 (SemanticCore.Class.cv nb068AlphaDummy408) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy449) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy449 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy450 (SemanticCore.Class.cv nb068AlphaDummy407) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy449) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_543 (f : SemanticCore.Var) :

nb068AlphaDummy454 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy451 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy452 f) (SemanticCore.Class.cv (nb068AlphaDummy410 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy451 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy451 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy452 f) (SemanticCore.Class.cv (nb068AlphaDummy409 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy451 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_544 :

nb068AlphaDummy489 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy485 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy486 (SemanticCore.Class.cv nb068AlphaDummy329) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy485) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy486)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy485 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy486 (SemanticCore.Class.cv nb068AlphaDummy328) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy485) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy486)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_545 (f : SemanticCore.Var) :

nb068AlphaDummy490 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy487 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy488 f) (SemanticCore.Class.cv (nb068AlphaDummy332 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy487 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy488 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy487 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy488 f) (SemanticCore.Class.cv (nb068AlphaDummy331 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy487 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy488 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_546 :

nb068AlphaDummy029 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy020)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy021)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_547 (x y : SemanticCore.Var) :

nb068AlphaDummy030 x y ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy023 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy024 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_548 :

nb068AlphaDummy077 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy068)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy069)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_549 (f : SemanticCore.Var) :

nb068AlphaDummy078 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy071 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy072 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_550 :

nb068AlphaDummy113 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy104)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy105)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_551 (f : SemanticCore.Var) :

nb068AlphaDummy114 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy107 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy108 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_552 :

nb068AlphaDummy155 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy146)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy147)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_553 (f : SemanticCore.Var) :

nb068AlphaDummy156 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy149 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy150 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_554 :

nb068AlphaDummy191 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy182)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy183)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_555 (f : SemanticCore.Var) :

nb068AlphaDummy192 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy185 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy186 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_556 :

nb068AlphaDummy227 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy218)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy219)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_557 (f : SemanticCore.Var) :

nb068AlphaDummy228 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy221 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy222 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_558 :

nb068AlphaDummy267 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy258)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy259)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_559 (f : SemanticCore.Var) :

nb068AlphaDummy268 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy261 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy262 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_560 :

nb068AlphaDummy311 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy302)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy303)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_561 (f : SemanticCore.Var) :

nb068AlphaDummy312 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy305 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy306 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_562 :

nb068AlphaDummy359 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy350)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy351)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_563 (f : SemanticCore.Var) :

nb068AlphaDummy360 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy353 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy354 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_564 :

nb068AlphaDummy395 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy386)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy387)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_565 (f : SemanticCore.Var) :

nb068AlphaDummy396 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy389 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy390 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_566 :

nb068AlphaDummy437 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy428)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy429)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_567 (f : SemanticCore.Var) :

nb068AlphaDummy438 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy431 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy432 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_568 :

nb068AlphaDummy473 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy464)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy465)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_569 (f : SemanticCore.Var) :

nb068AlphaDummy474 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy467 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy468 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_570 :

nb068AlphaDummy509 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy500)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy501)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_571 (f : SemanticCore.Var) :

nb068AlphaDummy510 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy503 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy504 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_572 :

nb068AlphaDummy037 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_573 (x y : SemanticCore.Var) :

nb068AlphaDummy038 x y ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_574 :

nb068AlphaDummy085 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_575 (f : SemanticCore.Var) :

nb068AlphaDummy086 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_576 :

nb068AlphaDummy121 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_577 (f : SemanticCore.Var) :

nb068AlphaDummy122 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_578 :

nb068AlphaDummy163 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_579 (f : SemanticCore.Var) :

nb068AlphaDummy164 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_580 :

nb068AlphaDummy199 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_581 (f : SemanticCore.Var) :

nb068AlphaDummy200 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_582 :

nb068AlphaDummy235 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_583 (f : SemanticCore.Var) :

nb068AlphaDummy236 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_584 :

nb068AlphaDummy275 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_585 (f : SemanticCore.Var) :

nb068AlphaDummy276 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_586 :

nb068AlphaDummy319 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_587 (f : SemanticCore.Var) :

nb068AlphaDummy320 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_588 :

nb068AlphaDummy367 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_589 (f : SemanticCore.Var) :

nb068AlphaDummy368 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_590 :

nb068AlphaDummy403 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_591 (f : SemanticCore.Var) :

nb068AlphaDummy404 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_592 :

nb068AlphaDummy445 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_593 (f : SemanticCore.Var) :

nb068AlphaDummy446 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_594 :

nb068AlphaDummy481 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_595 (f : SemanticCore.Var) :

nb068AlphaDummy482 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_596 :

nb068AlphaDummy517 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy486))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_597 (f : SemanticCore.Var) :

nb068AlphaDummy518 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy488 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_598 :

nb068AlphaDummy025 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy020) (SemanticCore.Class.cv nb068AlphaDummy021)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy020) (SemanticCore.Class.cv nb068AlphaDummy021)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_599 (x y : SemanticCore.Var) :

nb068AlphaDummy026 x y ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy023 x y)) (SemanticCore.Class.cv (nb068AlphaDummy024 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy023 x y)) (SemanticCore.Class.cv (nb068AlphaDummy024 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_600 :

nb068AlphaDummy073 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_601 (f : SemanticCore.Var) :

nb068AlphaDummy074 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_602 :

nb068AlphaDummy109 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_603 (f : SemanticCore.Var) :

nb068AlphaDummy110 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_604 :

nb068AlphaDummy151 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_605 (f : SemanticCore.Var) :

nb068AlphaDummy152 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_606 :

nb068AlphaDummy187 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_607 (f : SemanticCore.Var) :

nb068AlphaDummy188 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))).fv

Certificates from NAR4C068C001Part009.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_608 :

nb068AlphaDummy223 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy218) (SemanticCore.Class.cv nb068AlphaDummy219)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy218) (SemanticCore.Class.cv nb068AlphaDummy219)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_609 (f : SemanticCore.Var) :

nb068AlphaDummy224 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy221 f)) (SemanticCore.Class.cv (nb068AlphaDummy222 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy221 f)) (SemanticCore.Class.cv (nb068AlphaDummy222 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_610 :

nb068AlphaDummy263 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy258) (SemanticCore.Class.cv nb068AlphaDummy259)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy258) (SemanticCore.Class.cv nb068AlphaDummy259)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_611 (f : SemanticCore.Var) :

nb068AlphaDummy264 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy261 f)) (SemanticCore.Class.cv (nb068AlphaDummy262 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy261 f)) (SemanticCore.Class.cv (nb068AlphaDummy262 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_612 :

nb068AlphaDummy307 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy302) (SemanticCore.Class.cv nb068AlphaDummy303)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy302) (SemanticCore.Class.cv nb068AlphaDummy303)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_613 (f : SemanticCore.Var) :

nb068AlphaDummy308 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy305 f)) (SemanticCore.Class.cv (nb068AlphaDummy306 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy305 f)) (SemanticCore.Class.cv (nb068AlphaDummy306 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_614 :

nb068AlphaDummy355 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy350) (SemanticCore.Class.cv nb068AlphaDummy351)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy350) (SemanticCore.Class.cv nb068AlphaDummy351)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_615 (f : SemanticCore.Var) :

nb068AlphaDummy356 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy353 f)) (SemanticCore.Class.cv (nb068AlphaDummy354 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy353 f)) (SemanticCore.Class.cv (nb068AlphaDummy354 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_616 :

nb068AlphaDummy391 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy386) (SemanticCore.Class.cv nb068AlphaDummy387)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy386) (SemanticCore.Class.cv nb068AlphaDummy387)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_617 (f : SemanticCore.Var) :

nb068AlphaDummy392 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy389 f)) (SemanticCore.Class.cv (nb068AlphaDummy390 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy389 f)) (SemanticCore.Class.cv (nb068AlphaDummy390 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_618 :

nb068AlphaDummy433 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy428) (SemanticCore.Class.cv nb068AlphaDummy429)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy428) (SemanticCore.Class.cv nb068AlphaDummy429)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_619 (f : SemanticCore.Var) :

nb068AlphaDummy434 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy431 f)) (SemanticCore.Class.cv (nb068AlphaDummy432 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy431 f)) (SemanticCore.Class.cv (nb068AlphaDummy432 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_620 :

nb068AlphaDummy469 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy464) (SemanticCore.Class.cv nb068AlphaDummy465)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy464) (SemanticCore.Class.cv nb068AlphaDummy465)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_621 (f : SemanticCore.Var) :

nb068AlphaDummy470 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy467 f)) (SemanticCore.Class.cv (nb068AlphaDummy468 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy467 f)) (SemanticCore.Class.cv (nb068AlphaDummy468 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_622 :

nb068AlphaDummy505 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy500) (SemanticCore.Class.cv nb068AlphaDummy501)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy500) (SemanticCore.Class.cv nb068AlphaDummy501)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_623 (f : SemanticCore.Var) :

nb068AlphaDummy506 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy503 f)) (SemanticCore.Class.cv (nb068AlphaDummy504 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy503 f)) (SemanticCore.Class.cv (nb068AlphaDummy504 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_625 (f : SemanticCore.Var) :

nb068AlphaDummy042 f ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_626 :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_628 :

nb068AlphaDummy279 ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy002)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy002)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_629 (y f : SemanticCore.Var) :

nb068AlphaDummy280 y f ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv y)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_630 :

nb068AlphaDummy039 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_631 (x y : SemanticCore.Var) :

nb068AlphaDummy040 x y ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_632 :

nb068AlphaDummy087 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_633 (f : SemanticCore.Var) :

nb068AlphaDummy088 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_634 :

nb068AlphaDummy123 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_635 (f : SemanticCore.Var) :

nb068AlphaDummy124 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_636 :

nb068AlphaDummy165 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_637 (f : SemanticCore.Var) :

nb068AlphaDummy166 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_638 :

nb068AlphaDummy201 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_639 (f : SemanticCore.Var) :

nb068AlphaDummy202 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_640 :

nb068AlphaDummy237 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_641 (f : SemanticCore.Var) :

nb068AlphaDummy238 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_642 :

nb068AlphaDummy277 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_643 (f : SemanticCore.Var) :

nb068AlphaDummy278 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_644 :

nb068AlphaDummy321 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_645 (f : SemanticCore.Var) :

nb068AlphaDummy322 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_646 :

nb068AlphaDummy369 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_647 (f : SemanticCore.Var) :

nb068AlphaDummy370 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_648 :

nb068AlphaDummy405 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_649 (f : SemanticCore.Var) :

nb068AlphaDummy406 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_650 :

nb068AlphaDummy447 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_651 (f : SemanticCore.Var) :

nb068AlphaDummy448 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_652 :

nb068AlphaDummy483 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_653 (f : SemanticCore.Var) :

nb068AlphaDummy484 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_654 :

nb068AlphaDummy519 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy486)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy486)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_655 (f : SemanticCore.Var) :

nb068AlphaDummy520 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy488 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy488 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_656 :

nb068AlphaDummy281 ∉ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb068AlphaDummy000)).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_657 (y f : SemanticCore.Var) :

nb068AlphaDummy282 y f ∉ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_661 :

nb068AlphaDummy129 ∉ {nb068AlphaDummy125 } ∪ {nb068AlphaDummy126 } ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Class.cv nb068AlphaDummy000) (SemanticCore.Class.cv nb068AlphaDummy125)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_662 (f : SemanticCore.Var) :

nb068AlphaDummy130 f ∉ {nb068AlphaDummy127 f} ∪ {nb068AlphaDummy128 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb068AlphaDummy127 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_667 (x y f : SemanticCore.Var) :

nb068AlphaDummy004 x y f ∉ {x} ∪ {y} ∪ (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_668 :

nb068AlphaDummy000 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_669 :

nb068AlphaDummy001 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_fresh_670 :

nb068AlphaDummy002 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_671 :

nb068AlphaDummy000 ≠ nb068AlphaDummy001

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_672 :

nb068AlphaDummy000 ≠ nb068AlphaDummy002

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_distinct_673 :

nb068AlphaDummy001 ≠ nb068AlphaDummy002

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0001 (x y f : SemanticCore.Var) :

x ∈ {x} ∪ {y} ∪ (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0003 (x y f : SemanticCore.Var) :

y ∈ {x} ∪ {y} ∪ (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0004 :

nb068AlphaDummy001 ∈ (SemanticCore.Class.cv nb068AlphaDummy001).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0005 :

nb068AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy006 (SemanticCore.Class.cv nb068AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy005) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy006 (SemanticCore.Class.cv nb068AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0006 (x y : SemanticCore.Var) :

x ∈ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0007 (x y : SemanticCore.Var) :

x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy008 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy008 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0010 :

nb068AlphaDummy006 ∈ (SemanticCore.Class.cv nb068AlphaDummy006).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0011 (x y : SemanticCore.Var) :

nb068AlphaDummy008 x y ∈ (SemanticCore.Class.cv (nb068AlphaDummy008 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0012 :

nb068AlphaDummy013 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy013) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy013) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy013).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0014 :

nb068AlphaDummy013 ∈ (SemanticCore.Class.cv nb068AlphaDummy013).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0015 (x y : SemanticCore.Var) :

nb068AlphaDummy015 x y ∈ (SemanticCore.Class.cv (nb068AlphaDummy015 x y)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0016 :

nb068AlphaDummy020 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy020) (SemanticCore.Class.cv nb068AlphaDummy021)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy020) (SemanticCore.Class.cv nb068AlphaDummy021)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0017 (x y : SemanticCore.Var) :

nb068AlphaDummy023 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy023 x y)) (SemanticCore.Class.cv (nb068AlphaDummy024 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy023 x y)) (SemanticCore.Class.cv (nb068AlphaDummy024 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0018 :

nb068AlphaDummy020 ∈ (SemanticCore.Class.cv nb068AlphaDummy020).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy021).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0019 (x y : SemanticCore.Var) :

nb068AlphaDummy023 x y ∈ (SemanticCore.Class.cv (nb068AlphaDummy023 x y)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy024 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0020 :

nb068AlphaDummy021 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy020) (SemanticCore.Class.cv nb068AlphaDummy021)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy020) (SemanticCore.Class.cv nb068AlphaDummy021)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0021 (x y : SemanticCore.Var) :

nb068AlphaDummy024 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy023 x y)) (SemanticCore.Class.cv (nb068AlphaDummy024 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy023 x y)) (SemanticCore.Class.cv (nb068AlphaDummy024 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0022 :

nb068AlphaDummy021 ∈ (SemanticCore.Class.cv nb068AlphaDummy020).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy021).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0023 (x y : SemanticCore.Var) :

nb068AlphaDummy024 x y ∈ (SemanticCore.Class.cv (nb068AlphaDummy023 x y)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy024 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0024 :

nb068AlphaDummy020 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy020)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy021)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0025 (x y : SemanticCore.Var) :

nb068AlphaDummy023 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy023 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy024 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0026 :

nb068AlphaDummy020 ∈ (SemanticCore.Class.cv nb068AlphaDummy020).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy020).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0027 (x y : SemanticCore.Var) :

nb068AlphaDummy023 x y ∈ (SemanticCore.Class.cv (nb068AlphaDummy023 x y)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy023 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0028 :

nb068AlphaDummy021 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy020)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy021)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0029 (x y : SemanticCore.Var) :

nb068AlphaDummy024 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy023 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy024 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0030 :

nb068AlphaDummy021 ∈ (SemanticCore.Class.cv nb068AlphaDummy021).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy021).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0031 (x y : SemanticCore.Var) :

nb068AlphaDummy024 x y ∈ (SemanticCore.Class.cv (nb068AlphaDummy024 x y)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy024 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0032 :

nb068AlphaDummy002 ∈ (SemanticCore.Class.cv nb068AlphaDummy001).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0033 :

nb068AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy006 (SemanticCore.Class.cv nb068AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy005) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy006 (SemanticCore.Class.cv nb068AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0034 (x y : SemanticCore.Var) :

y ∈ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0035 (x y : SemanticCore.Var) :

y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy008 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy008 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0036 :

nb068AlphaDummy002 ∈ (SemanticCore.Class.cab nb068AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy006 (SemanticCore.Class.cv nb068AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy006 (SemanticCore.Class.cv nb068AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0037 (x y : SemanticCore.Var) :

y ∈ (SemanticCore.Class.cab (nb068AlphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy008 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy008 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0038 :

nb068AlphaDummy006 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0039 (x y : SemanticCore.Var) :

nb068AlphaDummy008 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0040 :

nb068AlphaDummy006 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy006)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0041 (x y : SemanticCore.Var) :

nb068AlphaDummy008 x y ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy008 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0046 :

nb068AlphaDummy045 ∈ (SemanticCore.Class.cv nb068AlphaDummy045).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy046).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0047 :

nb068AlphaDummy045 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy054 (SemanticCore.Class.cv nb068AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy054 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0048 (f : SemanticCore.Var) :

nb068AlphaDummy048 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy048 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy049 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0049 (f : SemanticCore.Var) :

nb068AlphaDummy048 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy056 f) (SemanticCore.Class.cv (nb068AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy056 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0051 (f : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0052 :

nb068AlphaDummy054 ∈ (SemanticCore.Class.cv nb068AlphaDummy054).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0053 (f : SemanticCore.Var) :

nb068AlphaDummy056 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy056 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0054 :

nb068AlphaDummy061 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy061) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy061) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy061).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0056 :

nb068AlphaDummy061 ∈ (SemanticCore.Class.cv nb068AlphaDummy061).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0057 (f : SemanticCore.Var) :

nb068AlphaDummy063 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy063 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0058 :

nb068AlphaDummy068 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0059 (f : SemanticCore.Var) :

nb068AlphaDummy071 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0060 :

nb068AlphaDummy068 ∈ (SemanticCore.Class.cv nb068AlphaDummy068).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy069).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0061 (f : SemanticCore.Var) :

nb068AlphaDummy071 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy071 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy072 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0062 :

nb068AlphaDummy069 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0063 (f : SemanticCore.Var) :

nb068AlphaDummy072 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0064 :

nb068AlphaDummy069 ∈ (SemanticCore.Class.cv nb068AlphaDummy068).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy069).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0065 (f : SemanticCore.Var) :

nb068AlphaDummy072 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy071 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy072 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0066 :

nb068AlphaDummy068 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy068)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy069)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0067 (f : SemanticCore.Var) :

nb068AlphaDummy071 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy071 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy072 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0068 :

nb068AlphaDummy068 ∈ (SemanticCore.Class.cv nb068AlphaDummy068).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy068).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0069 (f : SemanticCore.Var) :

nb068AlphaDummy071 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy071 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy071 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0070 :

nb068AlphaDummy069 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy068)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy069)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0071 (f : SemanticCore.Var) :

nb068AlphaDummy072 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy071 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy072 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0072 :

nb068AlphaDummy069 ∈ (SemanticCore.Class.cv nb068AlphaDummy069).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy069).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0073 (f : SemanticCore.Var) :

nb068AlphaDummy072 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy072 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy072 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0074 :

nb068AlphaDummy046 ∈ (SemanticCore.Class.cv nb068AlphaDummy045).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy046).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0075 :

nb068AlphaDummy046 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy054 (SemanticCore.Class.cv nb068AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy054 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv