Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C078C001Block003

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C078C001Part012.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_254 (h : SemanticCore.Var) :

nb078AlphaDummy1020 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1012 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_255 (h : SemanticCore.Var) :

nb078AlphaDummy1019 h ≠ nb078AlphaDummy1020 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_256 :

nb078AlphaDummy1023 ∉ (SemanticCore.Class.cv nb078AlphaDummy1017).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_257 :

nb078AlphaDummy1024 ∉ (SemanticCore.Class.cv nb078AlphaDummy1017).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_258 :

nb078AlphaDummy1025 ∉ (SemanticCore.Class.cv nb078AlphaDummy1017).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_259 :

nb078AlphaDummy1023 ≠ nb078AlphaDummy1024

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_260 :

nb078AlphaDummy1023 ≠ nb078AlphaDummy1025

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_261 :

nb078AlphaDummy1024 ≠ nb078AlphaDummy1025

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_262 (h : SemanticCore.Var) :

nb078AlphaDummy1026 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1019 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_263 (h : SemanticCore.Var) :

nb078AlphaDummy1027 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1019 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_264 (h : SemanticCore.Var) :

nb078AlphaDummy1028 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1019 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_265 (h : SemanticCore.Var) :

nb078AlphaDummy1026 h ≠ nb078AlphaDummy1027 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_266 (h : SemanticCore.Var) :

nb078AlphaDummy1026 h ≠ nb078AlphaDummy1028 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_267 (h : SemanticCore.Var) :

nb078AlphaDummy1027 h ≠ nb078AlphaDummy1028 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_268 :

nb078AlphaDummy1035 ∉ (SemanticCore.Class.cv nb078AlphaDummy1024).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1024).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_269 :

nb078AlphaDummy1031 ∉ (SemanticCore.Class.cv nb078AlphaDummy1024).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1025).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_270 :

nb078AlphaDummy1037 ∉ (SemanticCore.Class.cv nb078AlphaDummy1025).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1025).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_271 (h : SemanticCore.Var) :

nb078AlphaDummy1036 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1027 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1027 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_272 (h : SemanticCore.Var) :

nb078AlphaDummy1032 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1027 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1028 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_273 (h : SemanticCore.Var) :

nb078AlphaDummy1038 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1028 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1028 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_274 :

nb078AlphaDummy109 ∉ (SemanticCore.Class.cv nb078AlphaDummy103).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_275 :

nb078AlphaDummy110 ∉ (SemanticCore.Class.cv nb078AlphaDummy103).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_276 :

nb078AlphaDummy111 ∉ (SemanticCore.Class.cv nb078AlphaDummy103).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_277 :

nb078AlphaDummy109 ≠ nb078AlphaDummy110

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_278 :

nb078AlphaDummy109 ≠ nb078AlphaDummy111

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_279 :

nb078AlphaDummy110 ≠ nb078AlphaDummy111

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_280 :

nb078AlphaDummy1057 ∉ (SemanticCore.Class.cv nb078AlphaDummy1049).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1050).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_281 :

nb078AlphaDummy1058 ∉ (SemanticCore.Class.cv nb078AlphaDummy1049).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1050).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_282 :

nb078AlphaDummy1057 ≠ nb078AlphaDummy1058

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_283 :

nb078AlphaDummy1093 ∉ (SemanticCore.Class.cv nb078AlphaDummy1049).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1051).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_284 :

nb078AlphaDummy1094 ∉ (SemanticCore.Class.cv nb078AlphaDummy1049).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1051).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_285 :

nb078AlphaDummy1093 ≠ nb078AlphaDummy1094

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

nb078AlphaDummy112 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy105 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy113 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy105 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy114 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy105 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy112 f ≠ nb078AlphaDummy113 f

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

nb078AlphaDummy112 f ≠ nb078AlphaDummy114 f

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

nb078AlphaDummy113 f ≠ nb078AlphaDummy114 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_292 :

nb078AlphaDummy1207 ∉ (SemanticCore.Class.cv nb078AlphaDummy1051).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1050).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_293 :

nb078AlphaDummy1208 ∉ (SemanticCore.Class.cv nb078AlphaDummy1051).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1050).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_294 :

nb078AlphaDummy1207 ≠ nb078AlphaDummy1208

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_295 (h : SemanticCore.Var) :

nb078AlphaDummy1059 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1052 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1053 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_296 (h : SemanticCore.Var) :

nb078AlphaDummy1060 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1052 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1053 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_297 (h : SemanticCore.Var) :

nb078AlphaDummy1059 h ≠ nb078AlphaDummy1060 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_298 (h : SemanticCore.Var) :

nb078AlphaDummy1095 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1052 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1054 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_299 (h : SemanticCore.Var) :

nb078AlphaDummy1096 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1052 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1054 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_300 (h : SemanticCore.Var) :

nb078AlphaDummy1095 h ≠ nb078AlphaDummy1096 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_301 (h : SemanticCore.Var) :

nb078AlphaDummy1209 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1054 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1053 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_302 (h : SemanticCore.Var) :

nb078AlphaDummy1210 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1054 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1053 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_303 (h : SemanticCore.Var) :

nb078AlphaDummy1209 h ≠ nb078AlphaDummy1210 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_304 :

nb078AlphaDummy1065 ∉ (SemanticCore.Class.cv nb078AlphaDummy1058).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_305 :

nb078AlphaDummy1066 ∉ (SemanticCore.Class.cv nb078AlphaDummy1058).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_306 :

nb078AlphaDummy1065 ≠ nb078AlphaDummy1066

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_307 (h : SemanticCore.Var) :

nb078AlphaDummy1067 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1060 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_308 (h : SemanticCore.Var) :

nb078AlphaDummy1068 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1060 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_309 (h : SemanticCore.Var) :

nb078AlphaDummy1067 h ≠ nb078AlphaDummy1068 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_310 :

nb078AlphaDummy1071 ∉ (SemanticCore.Class.cv nb078AlphaDummy1065).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_311 :

nb078AlphaDummy1072 ∉ (SemanticCore.Class.cv nb078AlphaDummy1065).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_312 :

nb078AlphaDummy1073 ∉ (SemanticCore.Class.cv nb078AlphaDummy1065).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_313 :

nb078AlphaDummy1071 ≠ nb078AlphaDummy1072

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_314 :

nb078AlphaDummy1071 ≠ nb078AlphaDummy1073

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_315 :

nb078AlphaDummy1072 ≠ nb078AlphaDummy1073

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_316 (h : SemanticCore.Var) :

nb078AlphaDummy1074 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1067 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_317 (h : SemanticCore.Var) :

nb078AlphaDummy1075 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1067 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_318 (h : SemanticCore.Var) :

nb078AlphaDummy1076 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1067 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_319 (h : SemanticCore.Var) :

nb078AlphaDummy1074 h ≠ nb078AlphaDummy1075 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_320 (h : SemanticCore.Var) :

nb078AlphaDummy1074 h ≠ nb078AlphaDummy1076 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_321 (h : SemanticCore.Var) :

nb078AlphaDummy1075 h ≠ nb078AlphaDummy1076 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_322 :

nb078AlphaDummy1083 ∉ (SemanticCore.Class.cv nb078AlphaDummy1072).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1072).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_323 :

nb078AlphaDummy1079 ∉ (SemanticCore.Class.cv nb078AlphaDummy1072).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1073).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_324 :

nb078AlphaDummy1085 ∉ (SemanticCore.Class.cv nb078AlphaDummy1073).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1073).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_325 (h : SemanticCore.Var) :

nb078AlphaDummy1084 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1075 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1075 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_326 (h : SemanticCore.Var) :

nb078AlphaDummy1080 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1075 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1076 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_327 (h : SemanticCore.Var) :

nb078AlphaDummy1086 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1076 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1076 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_328 :

nb078AlphaDummy1101 ∉ (SemanticCore.Class.cv nb078AlphaDummy1094).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_329 :

nb078AlphaDummy1102 ∉ (SemanticCore.Class.cv nb078AlphaDummy1094).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_330 :

nb078AlphaDummy1101 ≠ nb078AlphaDummy1102

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_331 (h : SemanticCore.Var) :

nb078AlphaDummy1103 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1096 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_332 (h : SemanticCore.Var) :

nb078AlphaDummy1104 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1096 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_333 (h : SemanticCore.Var) :

nb078AlphaDummy1103 h ≠ nb078AlphaDummy1104 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_334 :

nb078AlphaDummy121 ∉ (SemanticCore.Class.cv nb078AlphaDummy110).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy110).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_335 :

nb078AlphaDummy117 ∉ (SemanticCore.Class.cv nb078AlphaDummy110).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy111).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_336 :

nb078AlphaDummy1107 ∉ (SemanticCore.Class.cv nb078AlphaDummy1101).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_337 :

nb078AlphaDummy1108 ∉ (SemanticCore.Class.cv nb078AlphaDummy1101).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_338 :

nb078AlphaDummy1109 ∉ (SemanticCore.Class.cv nb078AlphaDummy1101).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_339 :

nb078AlphaDummy1107 ≠ nb078AlphaDummy1108

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_340 :

nb078AlphaDummy1107 ≠ nb078AlphaDummy1109

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_341 :

nb078AlphaDummy1108 ≠ nb078AlphaDummy1109

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_342 (h : SemanticCore.Var) :

nb078AlphaDummy1110 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1103 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_343 (h : SemanticCore.Var) :

nb078AlphaDummy1111 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1103 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_344 (h : SemanticCore.Var) :

nb078AlphaDummy1112 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1103 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_345 (h : SemanticCore.Var) :

nb078AlphaDummy1110 h ≠ nb078AlphaDummy1111 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_346 (h : SemanticCore.Var) :

nb078AlphaDummy1110 h ≠ nb078AlphaDummy1112 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_347 (h : SemanticCore.Var) :

nb078AlphaDummy1111 h ≠ nb078AlphaDummy1112 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_348 :

nb078AlphaDummy1119 ∉ (SemanticCore.Class.cv nb078AlphaDummy1108).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1108).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_349 :

nb078AlphaDummy1115 ∉ (SemanticCore.Class.cv nb078AlphaDummy1108).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1109).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_350 :

nb078AlphaDummy1121 ∉ (SemanticCore.Class.cv nb078AlphaDummy1109).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1109).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_351 :

nb078AlphaDummy123 ∉ (SemanticCore.Class.cv nb078AlphaDummy111).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy111).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_352 (h : SemanticCore.Var) :

nb078AlphaDummy1120 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1111 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1111 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_353 (h : SemanticCore.Var) :

nb078AlphaDummy1116 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1111 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1112 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_354 (h : SemanticCore.Var) :

nb078AlphaDummy1122 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1112 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1112 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_355 :

nb078AlphaDummy1135 ∉ (SemanticCore.Class.cv nb078AlphaDummy1129).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1130).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_356 :

nb078AlphaDummy1136 ∉ (SemanticCore.Class.cv nb078AlphaDummy1129).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1130).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_357 :

nb078AlphaDummy1135 ≠ nb078AlphaDummy1136

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

nb078AlphaDummy122 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy113 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy113 f)).fv

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

nb078AlphaDummy118 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy113 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy114 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_360 :

nb078AlphaDummy1171 ∉ (SemanticCore.Class.cv nb078AlphaDummy1130).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1129).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_361 :

nb078AlphaDummy1172 ∉ (SemanticCore.Class.cv nb078AlphaDummy1130).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1129).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_362 :

nb078AlphaDummy1171 ≠ nb078AlphaDummy1172

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_363 (h : SemanticCore.Var) :

nb078AlphaDummy1137 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1131 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1132 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_364 (h : SemanticCore.Var) :

nb078AlphaDummy1138 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1131 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1132 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_365 (h : SemanticCore.Var) :

nb078AlphaDummy1137 h ≠ nb078AlphaDummy1138 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_366 (h : SemanticCore.Var) :

nb078AlphaDummy1173 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1132 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1131 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_367 (h : SemanticCore.Var) :

nb078AlphaDummy1174 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1132 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1131 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_368 (h : SemanticCore.Var) :

nb078AlphaDummy1173 h ≠ nb078AlphaDummy1174 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_369 :

nb078AlphaDummy1143 ∉ (SemanticCore.Class.cv nb078AlphaDummy1136).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_370 :

nb078AlphaDummy1144 ∉ (SemanticCore.Class.cv nb078AlphaDummy1136).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_371 :

nb078AlphaDummy1143 ≠ nb078AlphaDummy1144

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_372 (h : SemanticCore.Var) :

nb078AlphaDummy1145 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1138 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_373 (h : SemanticCore.Var) :

nb078AlphaDummy1146 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1138 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_374 (h : SemanticCore.Var) :

nb078AlphaDummy1145 h ≠ nb078AlphaDummy1146 h

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

nb078AlphaDummy124 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy114 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy114 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_376 :

nb078AlphaDummy1149 ∉ (SemanticCore.Class.cv nb078AlphaDummy1143).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_377 :

nb078AlphaDummy1150 ∉ (SemanticCore.Class.cv nb078AlphaDummy1143).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_378 :

nb078AlphaDummy1151 ∉ (SemanticCore.Class.cv nb078AlphaDummy1143).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_379 :

nb078AlphaDummy1149 ≠ nb078AlphaDummy1150

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_380 :

nb078AlphaDummy1149 ≠ nb078AlphaDummy1151

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_381 :

nb078AlphaDummy1150 ≠ nb078AlphaDummy1151

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_382 (h : SemanticCore.Var) :

nb078AlphaDummy1152 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1145 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_383 (h : SemanticCore.Var) :

nb078AlphaDummy1153 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1145 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_384 (h : SemanticCore.Var) :

nb078AlphaDummy1154 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1145 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_385 (h : SemanticCore.Var) :

nb078AlphaDummy1152 h ≠ nb078AlphaDummy1153 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_386 (h : SemanticCore.Var) :

nb078AlphaDummy1152 h ≠ nb078AlphaDummy1154 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_387 (h : SemanticCore.Var) :

nb078AlphaDummy1153 h ≠ nb078AlphaDummy1154 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_388 :

nb078AlphaDummy1161 ∉ (SemanticCore.Class.cv nb078AlphaDummy1150).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1150).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_389 :

nb078AlphaDummy1157 ∉ (SemanticCore.Class.cv nb078AlphaDummy1150).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1151).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_390 :

nb078AlphaDummy1163 ∉ (SemanticCore.Class.cv nb078AlphaDummy1151).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1151).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_391 (h : SemanticCore.Var) :

nb078AlphaDummy1162 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1153 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1153 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_392 (h : SemanticCore.Var) :

nb078AlphaDummy1158 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1153 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1154 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_393 (h : SemanticCore.Var) :

nb078AlphaDummy1164 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1154 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1154 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_394 :

nb078AlphaDummy1179 ∉ (SemanticCore.Class.cv nb078AlphaDummy1172).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_395 :

nb078AlphaDummy1180 ∉ (SemanticCore.Class.cv nb078AlphaDummy1172).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_396 :

nb078AlphaDummy1179 ≠ nb078AlphaDummy1180

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_397 (h : SemanticCore.Var) :

nb078AlphaDummy1181 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1174 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_398 (h : SemanticCore.Var) :

nb078AlphaDummy1182 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1174 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_399 (h : SemanticCore.Var) :

nb078AlphaDummy1181 h ≠ nb078AlphaDummy1182 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_400 :

nb078AlphaDummy1185 ∉ (SemanticCore.Class.cv nb078AlphaDummy1179).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_401 :

nb078AlphaDummy1186 ∉ (SemanticCore.Class.cv nb078AlphaDummy1179).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_402 :

nb078AlphaDummy1187 ∉ (SemanticCore.Class.cv nb078AlphaDummy1179).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_403 :

nb078AlphaDummy1185 ≠ nb078AlphaDummy1186

Certificates from NAR4C078C001Part013.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_404 :

nb078AlphaDummy1185 ≠ nb078AlphaDummy1187

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_405 :

nb078AlphaDummy1186 ≠ nb078AlphaDummy1187

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_406 (h : SemanticCore.Var) :

nb078AlphaDummy1188 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1181 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_407 (h : SemanticCore.Var) :

nb078AlphaDummy1189 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1181 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_408 (h : SemanticCore.Var) :

nb078AlphaDummy1190 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1181 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_409 (h : SemanticCore.Var) :

nb078AlphaDummy1188 h ≠ nb078AlphaDummy1189 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_410 (h : SemanticCore.Var) :

nb078AlphaDummy1188 h ≠ nb078AlphaDummy1190 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_411 (h : SemanticCore.Var) :

nb078AlphaDummy1189 h ≠ nb078AlphaDummy1190 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_412 :

nb078AlphaDummy1197 ∉ (SemanticCore.Class.cv nb078AlphaDummy1186).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1186).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_413 :

nb078AlphaDummy1193 ∉ (SemanticCore.Class.cv nb078AlphaDummy1186).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1187).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_414 :

nb078AlphaDummy1199 ∉ (SemanticCore.Class.cv nb078AlphaDummy1187).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1187).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_415 (h : SemanticCore.Var) :

nb078AlphaDummy1198 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1189 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1189 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_416 (h : SemanticCore.Var) :

nb078AlphaDummy1194 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1189 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1190 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_417 (h : SemanticCore.Var) :

nb078AlphaDummy1200 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1190 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1190 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_418 :

nb078AlphaDummy1215 ∉ (SemanticCore.Class.cv nb078AlphaDummy1208).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_419 :

nb078AlphaDummy1216 ∉ (SemanticCore.Class.cv nb078AlphaDummy1208).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_420 :

nb078AlphaDummy1215 ≠ nb078AlphaDummy1216

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_421 (h : SemanticCore.Var) :

nb078AlphaDummy1217 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1210 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_422 (h : SemanticCore.Var) :

nb078AlphaDummy1218 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1210 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_423 (h : SemanticCore.Var) :

nb078AlphaDummy1217 h ≠ nb078AlphaDummy1218 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_424 :

nb078AlphaDummy1221 ∉ (SemanticCore.Class.cv nb078AlphaDummy1215).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_425 :

nb078AlphaDummy1222 ∉ (SemanticCore.Class.cv nb078AlphaDummy1215).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_426 :

nb078AlphaDummy1223 ∉ (SemanticCore.Class.cv nb078AlphaDummy1215).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_427 :

nb078AlphaDummy1221 ≠ nb078AlphaDummy1222

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_428 :

nb078AlphaDummy1221 ≠ nb078AlphaDummy1223

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_429 :

nb078AlphaDummy1222 ≠ nb078AlphaDummy1223

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_430 (h : SemanticCore.Var) :

nb078AlphaDummy1224 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1217 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_431 (h : SemanticCore.Var) :

nb078AlphaDummy1225 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1217 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_432 (h : SemanticCore.Var) :

nb078AlphaDummy1226 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1217 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_433 (h : SemanticCore.Var) :

nb078AlphaDummy1224 h ≠ nb078AlphaDummy1225 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_434 (h : SemanticCore.Var) :

nb078AlphaDummy1224 h ≠ nb078AlphaDummy1226 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_435 (h : SemanticCore.Var) :

nb078AlphaDummy1225 h ≠ nb078AlphaDummy1226 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_436 :

nb078AlphaDummy1233 ∉ (SemanticCore.Class.cv nb078AlphaDummy1222).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1222).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_437 :

nb078AlphaDummy1229 ∉ (SemanticCore.Class.cv nb078AlphaDummy1222).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1223).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_438 :

nb078AlphaDummy1235 ∉ (SemanticCore.Class.cv nb078AlphaDummy1223).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1223).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_439 (h : SemanticCore.Var) :

nb078AlphaDummy1234 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1225 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1225 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_440 (h : SemanticCore.Var) :

nb078AlphaDummy1230 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1225 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1226 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_441 (h : SemanticCore.Var) :

nb078AlphaDummy1236 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy1226 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1226 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_442 :

nb078AlphaDummy139 ∉ (SemanticCore.Class.cv nb078AlphaDummy132).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_443 :

nb078AlphaDummy140 ∉ (SemanticCore.Class.cv nb078AlphaDummy132).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_444 :

nb078AlphaDummy139 ≠ nb078AlphaDummy140

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

nb078AlphaDummy141 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy134 f)).fv

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

nb078AlphaDummy142 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy134 f)).fv

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

nb078AlphaDummy141 f ≠ nb078AlphaDummy142 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_448 :

nb078AlphaDummy145 ∉ (SemanticCore.Class.cv nb078AlphaDummy139).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_449 :

nb078AlphaDummy146 ∉ (SemanticCore.Class.cv nb078AlphaDummy139).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_450 :

nb078AlphaDummy147 ∉ (SemanticCore.Class.cv nb078AlphaDummy139).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_451 :

nb078AlphaDummy145 ≠ nb078AlphaDummy146

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_452 :

nb078AlphaDummy145 ≠ nb078AlphaDummy147

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_453 :

nb078AlphaDummy146 ≠ nb078AlphaDummy147

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

nb078AlphaDummy148 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy141 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy149 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy141 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy150 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy141 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy148 f ≠ nb078AlphaDummy149 f

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

nb078AlphaDummy148 f ≠ nb078AlphaDummy150 f

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

nb078AlphaDummy149 f ≠ nb078AlphaDummy150 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_460 :

nb078AlphaDummy157 ∉ (SemanticCore.Class.cv nb078AlphaDummy146).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy146).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_461 :

nb078AlphaDummy153 ∉ (SemanticCore.Class.cv nb078AlphaDummy146).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy147).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_462 :

nb078AlphaDummy159 ∉ (SemanticCore.Class.cv nb078AlphaDummy147).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy147).fv

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

nb078AlphaDummy158 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy149 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy149 f)).fv

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

nb078AlphaDummy154 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy149 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy150 f)).fv

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

nb078AlphaDummy160 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy150 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy150 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_466 :

nb078AlphaDummy175 ∉ (SemanticCore.Class.cv nb078AlphaDummy168).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_467 :

nb078AlphaDummy176 ∉ (SemanticCore.Class.cv nb078AlphaDummy168).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_468 :

nb078AlphaDummy175 ≠ nb078AlphaDummy176

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

nb078AlphaDummy177 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy170 f)).fv

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

nb078AlphaDummy178 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy170 f)).fv

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

nb078AlphaDummy177 f ≠ nb078AlphaDummy178 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_472 :

nb078AlphaDummy181 ∉ (SemanticCore.Class.cv nb078AlphaDummy175).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_473 :

nb078AlphaDummy182 ∉ (SemanticCore.Class.cv nb078AlphaDummy175).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_474 :

nb078AlphaDummy183 ∉ (SemanticCore.Class.cv nb078AlphaDummy175).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_475 :

nb078AlphaDummy181 ≠ nb078AlphaDummy182

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_476 :

nb078AlphaDummy181 ≠ nb078AlphaDummy183

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_477 :

nb078AlphaDummy182 ≠ nb078AlphaDummy183

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

nb078AlphaDummy184 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy177 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy185 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy177 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy186 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy177 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy184 f ≠ nb078AlphaDummy185 f

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

nb078AlphaDummy184 f ≠ nb078AlphaDummy186 f

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

nb078AlphaDummy185 f ≠ nb078AlphaDummy186 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_484 :

nb078AlphaDummy193 ∉ (SemanticCore.Class.cv nb078AlphaDummy182).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy182).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_485 :

nb078AlphaDummy189 ∉ (SemanticCore.Class.cv nb078AlphaDummy182).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy183).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_486 :

nb078AlphaDummy195 ∉ (SemanticCore.Class.cv nb078AlphaDummy183).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy183).fv

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

nb078AlphaDummy194 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy185 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy185 f)).fv

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

nb078AlphaDummy190 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy185 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy186 f)).fv

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

nb078AlphaDummy196 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy186 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy186 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_490 :

nb078AlphaDummy207 ∉ (SemanticCore.Class.cv nb078AlphaDummy204).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy203).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_491 :

nb078AlphaDummy208 ∉ (SemanticCore.Class.cv nb078AlphaDummy204).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy203).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_492 :

nb078AlphaDummy207 ≠ nb078AlphaDummy208

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

nb078AlphaDummy209 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy206 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy205 f)).fv

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

nb078AlphaDummy210 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy206 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy205 f)).fv

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

nb078AlphaDummy209 f ≠ nb078AlphaDummy210 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_496 :

nb078AlphaDummy215 ∉ (SemanticCore.Class.cv nb078AlphaDummy208).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_497 :

nb078AlphaDummy216 ∉ (SemanticCore.Class.cv nb078AlphaDummy208).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_498 :

nb078AlphaDummy215 ≠ nb078AlphaDummy216

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

nb078AlphaDummy217 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy210 f)).fv

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

nb078AlphaDummy218 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy210 f)).fv

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

nb078AlphaDummy217 f ≠ nb078AlphaDummy218 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_502 :

nb078AlphaDummy221 ∉ (SemanticCore.Class.cv nb078AlphaDummy215).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_503 :

nb078AlphaDummy222 ∉ (SemanticCore.Class.cv nb078AlphaDummy215).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_504 :

nb078AlphaDummy223 ∉ (SemanticCore.Class.cv nb078AlphaDummy215).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_505 :

nb078AlphaDummy221 ≠ nb078AlphaDummy222

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_506 :

nb078AlphaDummy221 ≠ nb078AlphaDummy223

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_507 :

nb078AlphaDummy222 ≠ nb078AlphaDummy223

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

nb078AlphaDummy224 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy217 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy225 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy217 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy226 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy217 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy224 f ≠ nb078AlphaDummy225 f

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

nb078AlphaDummy224 f ≠ nb078AlphaDummy226 f

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

nb078AlphaDummy225 f ≠ nb078AlphaDummy226 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_514 :

nb078AlphaDummy233 ∉ (SemanticCore.Class.cv nb078AlphaDummy222).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy222).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_515 :

nb078AlphaDummy229 ∉ (SemanticCore.Class.cv nb078AlphaDummy222).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy223).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_516 :

nb078AlphaDummy235 ∉ (SemanticCore.Class.cv nb078AlphaDummy223).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy223).fv

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

nb078AlphaDummy234 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy225 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy225 f)).fv

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

nb078AlphaDummy230 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy225 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy226 f)).fv

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

nb078AlphaDummy236 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy226 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy226 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_520 :

nb078AlphaDummy247 ∉ (SemanticCore.Class.cv nb078AlphaDummy244).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy243).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_521 :

nb078AlphaDummy248 ∉ (SemanticCore.Class.cv nb078AlphaDummy244).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy243).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_522 :

nb078AlphaDummy247 ≠ nb078AlphaDummy248

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

nb078AlphaDummy249 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy246 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy245 f)).fv

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

nb078AlphaDummy250 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy246 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy245 f)).fv

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

nb078AlphaDummy249 f ≠ nb078AlphaDummy250 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_526 :

nb078AlphaDummy255 ∉ (SemanticCore.Class.cv nb078AlphaDummy248).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_527 :

nb078AlphaDummy256 ∉ (SemanticCore.Class.cv nb078AlphaDummy248).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_528 :

nb078AlphaDummy255 ≠ nb078AlphaDummy256

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

nb078AlphaDummy257 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy250 f)).fv

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

nb078AlphaDummy258 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy250 f)).fv

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

nb078AlphaDummy257 f ≠ nb078AlphaDummy258 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_532 :

nb078AlphaDummy261 ∉ (SemanticCore.Class.cv nb078AlphaDummy255).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_533 :

nb078AlphaDummy262 ∉ (SemanticCore.Class.cv nb078AlphaDummy255).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_534 :

nb078AlphaDummy263 ∉ (SemanticCore.Class.cv nb078AlphaDummy255).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_535 :

nb078AlphaDummy261 ≠ nb078AlphaDummy262

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_536 :

nb078AlphaDummy261 ≠ nb078AlphaDummy263

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_537 :

nb078AlphaDummy262 ≠ nb078AlphaDummy263

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

nb078AlphaDummy264 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy257 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy265 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy257 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy266 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy257 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

nb078AlphaDummy264 f ≠ nb078AlphaDummy265 f

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

nb078AlphaDummy264 f ≠ nb078AlphaDummy266 f

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

nb078AlphaDummy265 f ≠ nb078AlphaDummy266 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_544 :

nb078AlphaDummy273 ∉ (SemanticCore.Class.cv nb078AlphaDummy262).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy262).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_545 :

nb078AlphaDummy269 ∉ (SemanticCore.Class.cv nb078AlphaDummy262).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy263).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_546 :

nb078AlphaDummy275 ∉ (SemanticCore.Class.cv nb078AlphaDummy263).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy263).fv

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

nb078AlphaDummy274 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy265 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy265 f)).fv

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

nb078AlphaDummy270 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy265 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy266 f)).fv

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

nb078AlphaDummy276 f ∉ (SemanticCore.Class.cv (nb078AlphaDummy266 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy266 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_550 :

nb078AlphaDummy295 ∉ (SemanticCore.Class.cv nb078AlphaDummy287).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy288).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_551 :

nb078AlphaDummy296 ∉ (SemanticCore.Class.cv nb078AlphaDummy287).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy288).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_552 :

nb078AlphaDummy295 ≠ nb078AlphaDummy296

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_553 :

nb078AlphaDummy331 ∉ (SemanticCore.Class.cv nb078AlphaDummy287).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy289).fv

Certificates from NAR4C078C001Part014.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_554 :

nb078AlphaDummy332 ∉ (SemanticCore.Class.cv nb078AlphaDummy287).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy289).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_555 :

nb078AlphaDummy331 ≠ nb078AlphaDummy332

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_556 :

nb078AlphaDummy445 ∉ (SemanticCore.Class.cv nb078AlphaDummy289).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy288).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_557 :

nb078AlphaDummy446 ∉ (SemanticCore.Class.cv nb078AlphaDummy289).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy288).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_558 :

nb078AlphaDummy445 ≠ nb078AlphaDummy446

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_559 (g : SemanticCore.Var) :

nb078AlphaDummy297 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy290 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy291 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_560 (g : SemanticCore.Var) :

nb078AlphaDummy298 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy290 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy291 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_561 (g : SemanticCore.Var) :

nb078AlphaDummy297 g ≠ nb078AlphaDummy298 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_562 (g : SemanticCore.Var) :

nb078AlphaDummy333 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy290 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy292 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_563 (g : SemanticCore.Var) :

nb078AlphaDummy334 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy290 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy292 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_564 (g : SemanticCore.Var) :

nb078AlphaDummy333 g ≠ nb078AlphaDummy334 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_565 (g : SemanticCore.Var) :

nb078AlphaDummy447 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy292 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy291 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_566 (g : SemanticCore.Var) :

nb078AlphaDummy448 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy292 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy291 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_567 (g : SemanticCore.Var) :

nb078AlphaDummy447 g ≠ nb078AlphaDummy448 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_568 :

nb078AlphaDummy303 ∉ (SemanticCore.Class.cv nb078AlphaDummy296).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_569 :

nb078AlphaDummy304 ∉ (SemanticCore.Class.cv nb078AlphaDummy296).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_570 :

nb078AlphaDummy303 ≠ nb078AlphaDummy304

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_571 (g : SemanticCore.Var) :

nb078AlphaDummy305 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy298 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_572 (g : SemanticCore.Var) :

nb078AlphaDummy306 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy298 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_573 (g : SemanticCore.Var) :

nb078AlphaDummy305 g ≠ nb078AlphaDummy306 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_574 :

nb078AlphaDummy309 ∉ (SemanticCore.Class.cv nb078AlphaDummy303).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_575 :

nb078AlphaDummy310 ∉ (SemanticCore.Class.cv nb078AlphaDummy303).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_576 :

nb078AlphaDummy311 ∉ (SemanticCore.Class.cv nb078AlphaDummy303).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_577 :

nb078AlphaDummy309 ≠ nb078AlphaDummy310

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_578 :

nb078AlphaDummy309 ≠ nb078AlphaDummy311

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_579 :

nb078AlphaDummy310 ≠ nb078AlphaDummy311

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_580 (g : SemanticCore.Var) :

nb078AlphaDummy312 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy305 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_581 (g : SemanticCore.Var) :

nb078AlphaDummy313 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy305 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_582 (g : SemanticCore.Var) :

nb078AlphaDummy314 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy305 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_583 (g : SemanticCore.Var) :

nb078AlphaDummy312 g ≠ nb078AlphaDummy313 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_584 (g : SemanticCore.Var) :

nb078AlphaDummy312 g ≠ nb078AlphaDummy314 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_585 (g : SemanticCore.Var) :

nb078AlphaDummy313 g ≠ nb078AlphaDummy314 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_586 :

nb078AlphaDummy321 ∉ (SemanticCore.Class.cv nb078AlphaDummy310).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy310).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_587 :

nb078AlphaDummy317 ∉ (SemanticCore.Class.cv nb078AlphaDummy310).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy311).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_588 :

nb078AlphaDummy323 ∉ (SemanticCore.Class.cv nb078AlphaDummy311).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy311).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_589 (g : SemanticCore.Var) :

nb078AlphaDummy322 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy313 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy313 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_590 (g : SemanticCore.Var) :

nb078AlphaDummy318 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy313 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy314 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_591 (g : SemanticCore.Var) :

nb078AlphaDummy324 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy314 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy314 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_592 :

nb078AlphaDummy339 ∉ (SemanticCore.Class.cv nb078AlphaDummy332).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_593 :

nb078AlphaDummy340 ∉ (SemanticCore.Class.cv nb078AlphaDummy332).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_594 :

nb078AlphaDummy339 ≠ nb078AlphaDummy340

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_595 (g : SemanticCore.Var) :

nb078AlphaDummy341 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy334 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_596 (g : SemanticCore.Var) :

nb078AlphaDummy342 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy334 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_597 (g : SemanticCore.Var) :

nb078AlphaDummy341 g ≠ nb078AlphaDummy342 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_598 :

nb078AlphaDummy345 ∉ (SemanticCore.Class.cv nb078AlphaDummy339).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_599 :

nb078AlphaDummy346 ∉ (SemanticCore.Class.cv nb078AlphaDummy339).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_600 :

nb078AlphaDummy347 ∉ (SemanticCore.Class.cv nb078AlphaDummy339).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_601 :

nb078AlphaDummy345 ≠ nb078AlphaDummy346

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_602 :

nb078AlphaDummy345 ≠ nb078AlphaDummy347

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_603 :

nb078AlphaDummy346 ≠ nb078AlphaDummy347

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_604 (g : SemanticCore.Var) :

nb078AlphaDummy348 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy341 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_605 (g : SemanticCore.Var) :

nb078AlphaDummy349 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy341 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_606 (g : SemanticCore.Var) :

nb078AlphaDummy350 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy341 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_607 (g : SemanticCore.Var) :

nb078AlphaDummy348 g ≠ nb078AlphaDummy349 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_608 (g : SemanticCore.Var) :

nb078AlphaDummy348 g ≠ nb078AlphaDummy350 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_609 (g : SemanticCore.Var) :

nb078AlphaDummy349 g ≠ nb078AlphaDummy350 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_610 :

nb078AlphaDummy357 ∉ (SemanticCore.Class.cv nb078AlphaDummy346).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy346).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_611 :

nb078AlphaDummy353 ∉ (SemanticCore.Class.cv nb078AlphaDummy346).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy347).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_612 :

nb078AlphaDummy359 ∉ (SemanticCore.Class.cv nb078AlphaDummy347).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy347).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_613 (g : SemanticCore.Var) :

nb078AlphaDummy358 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy349 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy349 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_614 (g : SemanticCore.Var) :

nb078AlphaDummy354 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy349 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy350 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_615 (g : SemanticCore.Var) :

nb078AlphaDummy360 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy350 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy350 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_616 :

nb078AlphaDummy373 ∉ (SemanticCore.Class.cv nb078AlphaDummy367).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy368).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_617 :

nb078AlphaDummy374 ∉ (SemanticCore.Class.cv nb078AlphaDummy367).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy368).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_618 :

nb078AlphaDummy373 ≠ nb078AlphaDummy374

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_619 :

nb078AlphaDummy409 ∉ (SemanticCore.Class.cv nb078AlphaDummy368).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy367).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_620 :

nb078AlphaDummy410 ∉ (SemanticCore.Class.cv nb078AlphaDummy368).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy367).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_621 :

nb078AlphaDummy409 ≠ nb078AlphaDummy410

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_622 (g : SemanticCore.Var) :

nb078AlphaDummy375 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy369 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy370 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_623 (g : SemanticCore.Var) :

nb078AlphaDummy376 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy369 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy370 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_624 (g : SemanticCore.Var) :

nb078AlphaDummy375 g ≠ nb078AlphaDummy376 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_625 (g : SemanticCore.Var) :

nb078AlphaDummy411 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy370 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy369 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_626 (g : SemanticCore.Var) :

nb078AlphaDummy412 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy370 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy369 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_627 (g : SemanticCore.Var) :

nb078AlphaDummy411 g ≠ nb078AlphaDummy412 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_628 :

nb078AlphaDummy381 ∉ (SemanticCore.Class.cv nb078AlphaDummy374).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_629 :

nb078AlphaDummy382 ∉ (SemanticCore.Class.cv nb078AlphaDummy374).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_630 :

nb078AlphaDummy381 ≠ nb078AlphaDummy382

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_631 (g : SemanticCore.Var) :

nb078AlphaDummy383 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy376 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_632 (g : SemanticCore.Var) :

nb078AlphaDummy384 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy376 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_633 (g : SemanticCore.Var) :

nb078AlphaDummy383 g ≠ nb078AlphaDummy384 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_634 :

nb078AlphaDummy387 ∉ (SemanticCore.Class.cv nb078AlphaDummy381).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_635 :

nb078AlphaDummy388 ∉ (SemanticCore.Class.cv nb078AlphaDummy381).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_636 :

nb078AlphaDummy389 ∉ (SemanticCore.Class.cv nb078AlphaDummy381).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_637 :

nb078AlphaDummy387 ≠ nb078AlphaDummy388

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_638 :

nb078AlphaDummy387 ≠ nb078AlphaDummy389

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_639 :

nb078AlphaDummy388 ≠ nb078AlphaDummy389

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_640 (g : SemanticCore.Var) :

nb078AlphaDummy390 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy383 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_641 (g : SemanticCore.Var) :

nb078AlphaDummy391 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy383 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_642 (g : SemanticCore.Var) :

nb078AlphaDummy392 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy383 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_643 (g : SemanticCore.Var) :

nb078AlphaDummy390 g ≠ nb078AlphaDummy391 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_644 (g : SemanticCore.Var) :

nb078AlphaDummy390 g ≠ nb078AlphaDummy392 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_645 (g : SemanticCore.Var) :

nb078AlphaDummy391 g ≠ nb078AlphaDummy392 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_646 :

nb078AlphaDummy399 ∉ (SemanticCore.Class.cv nb078AlphaDummy388).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy388).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_647 :

nb078AlphaDummy395 ∉ (SemanticCore.Class.cv nb078AlphaDummy388).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy389).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_648 :

nb078AlphaDummy401 ∉ (SemanticCore.Class.cv nb078AlphaDummy389).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy389).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_649 (g : SemanticCore.Var) :

nb078AlphaDummy400 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy391 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy391 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_650 (g : SemanticCore.Var) :

nb078AlphaDummy396 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy391 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy392 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_651 (g : SemanticCore.Var) :

nb078AlphaDummy402 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy392 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy392 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_652 :

nb078AlphaDummy417 ∉ (SemanticCore.Class.cv nb078AlphaDummy410).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_653 :

nb078AlphaDummy418 ∉ (SemanticCore.Class.cv nb078AlphaDummy410).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_654 :

nb078AlphaDummy417 ≠ nb078AlphaDummy418

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_655 (g : SemanticCore.Var) :

nb078AlphaDummy419 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy412 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_656 (g : SemanticCore.Var) :

nb078AlphaDummy420 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy412 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_657 (g : SemanticCore.Var) :

nb078AlphaDummy419 g ≠ nb078AlphaDummy420 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_658 :

nb078AlphaDummy423 ∉ (SemanticCore.Class.cv nb078AlphaDummy417).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_659 :

nb078AlphaDummy424 ∉ (SemanticCore.Class.cv nb078AlphaDummy417).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_660 :

nb078AlphaDummy425 ∉ (SemanticCore.Class.cv nb078AlphaDummy417).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_661 :

nb078AlphaDummy423 ≠ nb078AlphaDummy424

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_662 :

nb078AlphaDummy423 ≠ nb078AlphaDummy425

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_663 :

nb078AlphaDummy424 ≠ nb078AlphaDummy425

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_664 (g : SemanticCore.Var) :

nb078AlphaDummy426 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy419 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_665 (g : SemanticCore.Var) :

nb078AlphaDummy427 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy419 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_666 (g : SemanticCore.Var) :

nb078AlphaDummy428 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy419 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_667 (g : SemanticCore.Var) :

nb078AlphaDummy426 g ≠ nb078AlphaDummy427 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_668 (g : SemanticCore.Var) :

nb078AlphaDummy426 g ≠ nb078AlphaDummy428 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_669 (g : SemanticCore.Var) :

nb078AlphaDummy427 g ≠ nb078AlphaDummy428 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_670 :

nb078AlphaDummy435 ∉ (SemanticCore.Class.cv nb078AlphaDummy424).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy424).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_671 :

nb078AlphaDummy431 ∉ (SemanticCore.Class.cv nb078AlphaDummy424).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy425).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_672 :

nb078AlphaDummy437 ∉ (SemanticCore.Class.cv nb078AlphaDummy425).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy425).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_673 (g : SemanticCore.Var) :

nb078AlphaDummy436 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy427 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy427 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_674 (g : SemanticCore.Var) :

nb078AlphaDummy432 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy427 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy428 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_675 (g : SemanticCore.Var) :

nb078AlphaDummy438 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy428 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy428 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_676 :

nb078AlphaDummy453 ∉ (SemanticCore.Class.cv nb078AlphaDummy446).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_677 :

nb078AlphaDummy454 ∉ (SemanticCore.Class.cv nb078AlphaDummy446).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_678 :

nb078AlphaDummy453 ≠ nb078AlphaDummy454

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_679 (g : SemanticCore.Var) :

nb078AlphaDummy455 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy448 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_680 (g : SemanticCore.Var) :

nb078AlphaDummy456 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy448 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_681 (g : SemanticCore.Var) :

nb078AlphaDummy455 g ≠ nb078AlphaDummy456 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_682 :

nb078AlphaDummy459 ∉ (SemanticCore.Class.cv nb078AlphaDummy453).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_683 :

nb078AlphaDummy460 ∉ (SemanticCore.Class.cv nb078AlphaDummy453).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_684 :

nb078AlphaDummy461 ∉ (SemanticCore.Class.cv nb078AlphaDummy453).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_685 :

nb078AlphaDummy459 ≠ nb078AlphaDummy460

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_686 :

nb078AlphaDummy459 ≠ nb078AlphaDummy461

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_687 :

nb078AlphaDummy460 ≠ nb078AlphaDummy461

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_688 (g : SemanticCore.Var) :

nb078AlphaDummy462 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy455 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_689 (g : SemanticCore.Var) :

nb078AlphaDummy463 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy455 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_690 (g : SemanticCore.Var) :

nb078AlphaDummy464 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy455 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_691 (g : SemanticCore.Var) :

nb078AlphaDummy462 g ≠ nb078AlphaDummy463 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_692 (g : SemanticCore.Var) :

nb078AlphaDummy462 g ≠ nb078AlphaDummy464 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_693 (g : SemanticCore.Var) :

nb078AlphaDummy463 g ≠ nb078AlphaDummy464 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_694 :

nb078AlphaDummy471 ∉ (SemanticCore.Class.cv nb078AlphaDummy460).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy460).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_695 :

nb078AlphaDummy467 ∉ (SemanticCore.Class.cv nb078AlphaDummy460).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy461).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_696 :

nb078AlphaDummy473 ∉ (SemanticCore.Class.cv nb078AlphaDummy461).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy461).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_697 (g : SemanticCore.Var) :

nb078AlphaDummy472 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy463 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy463 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_698 (g : SemanticCore.Var) :

nb078AlphaDummy468 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy463 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy464 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_699 (g : SemanticCore.Var) :

nb078AlphaDummy474 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy464 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy464 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_700 :

nb078AlphaDummy485 ∉ (SemanticCore.Class.cv nb078AlphaDummy482).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy481).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_701 :

nb078AlphaDummy486 ∉ (SemanticCore.Class.cv nb078AlphaDummy482).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy481).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_702 :

nb078AlphaDummy485 ≠ nb078AlphaDummy486

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_703 (g : SemanticCore.Var) :

nb078AlphaDummy487 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy484 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy483 g)).fv

Certificates from NAR4C078C001Part015.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_704 (g : SemanticCore.Var) :

nb078AlphaDummy488 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy484 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy483 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_705 (g : SemanticCore.Var) :

nb078AlphaDummy487 g ≠ nb078AlphaDummy488 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_706 :

nb078AlphaDummy493 ∉ (SemanticCore.Class.cv nb078AlphaDummy486).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_707 :

nb078AlphaDummy494 ∉ (SemanticCore.Class.cv nb078AlphaDummy486).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_708 :

nb078AlphaDummy493 ≠ nb078AlphaDummy494

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_709 (g : SemanticCore.Var) :

nb078AlphaDummy495 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy488 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_710 (g : SemanticCore.Var) :

nb078AlphaDummy496 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy488 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_711 (g : SemanticCore.Var) :

nb078AlphaDummy495 g ≠ nb078AlphaDummy496 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_712 :

nb078AlphaDummy499 ∉ (SemanticCore.Class.cv nb078AlphaDummy493).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_713 :

nb078AlphaDummy500 ∉ (SemanticCore.Class.cv nb078AlphaDummy493).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_714 :

nb078AlphaDummy501 ∉ (SemanticCore.Class.cv nb078AlphaDummy493).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_715 :

nb078AlphaDummy499 ≠ nb078AlphaDummy500

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_716 :

nb078AlphaDummy499 ≠ nb078AlphaDummy501

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_717 :

nb078AlphaDummy500 ≠ nb078AlphaDummy501

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_718 (g : SemanticCore.Var) :

nb078AlphaDummy502 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy495 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_719 (g : SemanticCore.Var) :

nb078AlphaDummy503 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy495 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_720 (g : SemanticCore.Var) :

nb078AlphaDummy504 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy495 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_721 (g : SemanticCore.Var) :

nb078AlphaDummy502 g ≠ nb078AlphaDummy503 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_722 (g : SemanticCore.Var) :

nb078AlphaDummy502 g ≠ nb078AlphaDummy504 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_723 (g : SemanticCore.Var) :

nb078AlphaDummy503 g ≠ nb078AlphaDummy504 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_724 :

nb078AlphaDummy511 ∉ (SemanticCore.Class.cv nb078AlphaDummy500).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy500).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_725 :

nb078AlphaDummy507 ∉ (SemanticCore.Class.cv nb078AlphaDummy500).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy501).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_726 :

nb078AlphaDummy513 ∉ (SemanticCore.Class.cv nb078AlphaDummy501).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy501).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_727 (g : SemanticCore.Var) :

nb078AlphaDummy512 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy503 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy503 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_728 (g : SemanticCore.Var) :

nb078AlphaDummy508 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy503 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy504 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_729 (g : SemanticCore.Var) :

nb078AlphaDummy514 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy504 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy504 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_730 :

nb078AlphaDummy529 ∉ (SemanticCore.Class.cv nb078AlphaDummy526).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy525).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_731 :

nb078AlphaDummy530 ∉ (SemanticCore.Class.cv nb078AlphaDummy526).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy525).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_732 :

nb078AlphaDummy529 ≠ nb078AlphaDummy530

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_733 (g : SemanticCore.Var) :

nb078AlphaDummy531 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy528 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy527 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_734 (g : SemanticCore.Var) :

nb078AlphaDummy532 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy528 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy527 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_735 (g : SemanticCore.Var) :

nb078AlphaDummy531 g ≠ nb078AlphaDummy532 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_736 :

nb078AlphaDummy537 ∉ (SemanticCore.Class.cv nb078AlphaDummy530).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_737 :

nb078AlphaDummy538 ∉ (SemanticCore.Class.cv nb078AlphaDummy530).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_738 :

nb078AlphaDummy537 ≠ nb078AlphaDummy538

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_739 (g : SemanticCore.Var) :

nb078AlphaDummy539 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy532 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_740 (g : SemanticCore.Var) :

nb078AlphaDummy540 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy532 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_741 (g : SemanticCore.Var) :

nb078AlphaDummy539 g ≠ nb078AlphaDummy540 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_742 :

nb078AlphaDummy543 ∉ (SemanticCore.Class.cv nb078AlphaDummy537).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_743 :

nb078AlphaDummy544 ∉ (SemanticCore.Class.cv nb078AlphaDummy537).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_744 :

nb078AlphaDummy545 ∉ (SemanticCore.Class.cv nb078AlphaDummy537).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_745 :

nb078AlphaDummy543 ≠ nb078AlphaDummy544

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_746 :

nb078AlphaDummy543 ≠ nb078AlphaDummy545

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_747 :

nb078AlphaDummy544 ≠ nb078AlphaDummy545

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_748 (g : SemanticCore.Var) :

nb078AlphaDummy546 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy539 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_749 (g : SemanticCore.Var) :

nb078AlphaDummy547 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy539 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_750 (g : SemanticCore.Var) :

nb078AlphaDummy548 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy539 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_751 (g : SemanticCore.Var) :

nb078AlphaDummy546 g ≠ nb078AlphaDummy547 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_752 (g : SemanticCore.Var) :

nb078AlphaDummy546 g ≠ nb078AlphaDummy548 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_753 (g : SemanticCore.Var) :

nb078AlphaDummy547 g ≠ nb078AlphaDummy548 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_754 :

nb078AlphaDummy555 ∉ (SemanticCore.Class.cv nb078AlphaDummy544).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy544).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_755 :

nb078AlphaDummy551 ∉ (SemanticCore.Class.cv nb078AlphaDummy544).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy545).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_756 :

nb078AlphaDummy557 ∉ (SemanticCore.Class.cv nb078AlphaDummy545).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy545).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_757 (g : SemanticCore.Var) :

nb078AlphaDummy556 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy547 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy547 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_758 (g : SemanticCore.Var) :

nb078AlphaDummy552 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy547 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy548 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_759 (g : SemanticCore.Var) :

nb078AlphaDummy558 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy548 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy548 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_760 :

nb078AlphaDummy577 ∉ (SemanticCore.Class.cv nb078AlphaDummy569).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy570).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_761 :

nb078AlphaDummy578 ∉ (SemanticCore.Class.cv nb078AlphaDummy569).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy570).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_762 :

nb078AlphaDummy577 ≠ nb078AlphaDummy578

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_763 :

nb078AlphaDummy613 ∉ (SemanticCore.Class.cv nb078AlphaDummy569).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy571).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_764 :

nb078AlphaDummy614 ∉ (SemanticCore.Class.cv nb078AlphaDummy569).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy571).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_765 :

nb078AlphaDummy613 ≠ nb078AlphaDummy614

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_766 :

nb078AlphaDummy727 ∉ (SemanticCore.Class.cv nb078AlphaDummy571).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy570).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_767 :

nb078AlphaDummy728 ∉ (SemanticCore.Class.cv nb078AlphaDummy571).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy570).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_768 :

nb078AlphaDummy727 ≠ nb078AlphaDummy728

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_769 (g : SemanticCore.Var) :

nb078AlphaDummy579 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy572 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy573 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_770 (g : SemanticCore.Var) :

nb078AlphaDummy580 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy572 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy573 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_771 (g : SemanticCore.Var) :

nb078AlphaDummy579 g ≠ nb078AlphaDummy580 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_772 (g : SemanticCore.Var) :

nb078AlphaDummy615 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy572 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy574 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_773 (g : SemanticCore.Var) :

nb078AlphaDummy616 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy572 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy574 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_774 (g : SemanticCore.Var) :

nb078AlphaDummy615 g ≠ nb078AlphaDummy616 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_775 (g : SemanticCore.Var) :

nb078AlphaDummy729 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy574 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy573 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_776 (g : SemanticCore.Var) :

nb078AlphaDummy730 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy574 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy573 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_777 (g : SemanticCore.Var) :

nb078AlphaDummy729 g ≠ nb078AlphaDummy730 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_778 :

nb078AlphaDummy585 ∉ (SemanticCore.Class.cv nb078AlphaDummy578).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_779 :

nb078AlphaDummy586 ∉ (SemanticCore.Class.cv nb078AlphaDummy578).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_780 :

nb078AlphaDummy585 ≠ nb078AlphaDummy586

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_781 (g : SemanticCore.Var) :

nb078AlphaDummy587 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy580 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_782 (g : SemanticCore.Var) :

nb078AlphaDummy588 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy580 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_783 (g : SemanticCore.Var) :

nb078AlphaDummy587 g ≠ nb078AlphaDummy588 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_784 :

nb078AlphaDummy591 ∉ (SemanticCore.Class.cv nb078AlphaDummy585).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_785 :

nb078AlphaDummy592 ∉ (SemanticCore.Class.cv nb078AlphaDummy585).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_786 :

nb078AlphaDummy593 ∉ (SemanticCore.Class.cv nb078AlphaDummy585).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_787 :

nb078AlphaDummy591 ≠ nb078AlphaDummy592

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_788 :

nb078AlphaDummy591 ≠ nb078AlphaDummy593

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_789 :

nb078AlphaDummy592 ≠ nb078AlphaDummy593

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_790 (g : SemanticCore.Var) :

nb078AlphaDummy594 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy587 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_791 (g : SemanticCore.Var) :

nb078AlphaDummy595 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy587 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_792 (g : SemanticCore.Var) :

nb078AlphaDummy596 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy587 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_793 (g : SemanticCore.Var) :

nb078AlphaDummy594 g ≠ nb078AlphaDummy595 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_794 (g : SemanticCore.Var) :

nb078AlphaDummy594 g ≠ nb078AlphaDummy596 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_795 (g : SemanticCore.Var) :

nb078AlphaDummy595 g ≠ nb078AlphaDummy596 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_796 :

nb078AlphaDummy603 ∉ (SemanticCore.Class.cv nb078AlphaDummy592).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy592).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_797 :

nb078AlphaDummy599 ∉ (SemanticCore.Class.cv nb078AlphaDummy592).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy593).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_798 :

nb078AlphaDummy605 ∉ (SemanticCore.Class.cv nb078AlphaDummy593).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy593).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_799 (g : SemanticCore.Var) :

nb078AlphaDummy604 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy595 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy595 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_800 (g : SemanticCore.Var) :

nb078AlphaDummy600 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy595 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy596 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_801 (g : SemanticCore.Var) :

nb078AlphaDummy606 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy596 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy596 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_802 :

nb078AlphaDummy621 ∉ (SemanticCore.Class.cv nb078AlphaDummy614).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_803 :

nb078AlphaDummy622 ∉ (SemanticCore.Class.cv nb078AlphaDummy614).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_804 :

nb078AlphaDummy621 ≠ nb078AlphaDummy622

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_805 (g : SemanticCore.Var) :

nb078AlphaDummy623 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy616 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_806 (g : SemanticCore.Var) :

nb078AlphaDummy624 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy616 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_807 (g : SemanticCore.Var) :

nb078AlphaDummy623 g ≠ nb078AlphaDummy624 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_808 :

nb078AlphaDummy627 ∉ (SemanticCore.Class.cv nb078AlphaDummy621).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_809 :

nb078AlphaDummy628 ∉ (SemanticCore.Class.cv nb078AlphaDummy621).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_810 :

nb078AlphaDummy629 ∉ (SemanticCore.Class.cv nb078AlphaDummy621).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_811 :

nb078AlphaDummy627 ≠ nb078AlphaDummy628

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_812 :

nb078AlphaDummy627 ≠ nb078AlphaDummy629

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_813 :

nb078AlphaDummy628 ≠ nb078AlphaDummy629

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_814 (g : SemanticCore.Var) :

nb078AlphaDummy630 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy623 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_815 (g : SemanticCore.Var) :

nb078AlphaDummy631 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy623 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_816 (g : SemanticCore.Var) :

nb078AlphaDummy632 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy623 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_817 (g : SemanticCore.Var) :

nb078AlphaDummy630 g ≠ nb078AlphaDummy631 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_818 (g : SemanticCore.Var) :

nb078AlphaDummy630 g ≠ nb078AlphaDummy632 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_819 (g : SemanticCore.Var) :

nb078AlphaDummy631 g ≠ nb078AlphaDummy632 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_820 :

nb078AlphaDummy639 ∉ (SemanticCore.Class.cv nb078AlphaDummy628).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy628).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_821 :

nb078AlphaDummy635 ∉ (SemanticCore.Class.cv nb078AlphaDummy628).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy629).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_822 :

nb078AlphaDummy641 ∉ (SemanticCore.Class.cv nb078AlphaDummy629).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy629).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_823 (g : SemanticCore.Var) :

nb078AlphaDummy640 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy631 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy631 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_824 (g : SemanticCore.Var) :

nb078AlphaDummy636 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy631 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy632 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_825 (g : SemanticCore.Var) :

nb078AlphaDummy642 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy632 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy632 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_826 :

nb078AlphaDummy655 ∉ (SemanticCore.Class.cv nb078AlphaDummy649).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy650).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_827 :

nb078AlphaDummy656 ∉ (SemanticCore.Class.cv nb078AlphaDummy649).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy650).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_828 :

nb078AlphaDummy655 ≠ nb078AlphaDummy656

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_829 :

nb078AlphaDummy691 ∉ (SemanticCore.Class.cv nb078AlphaDummy650).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy649).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_830 :

nb078AlphaDummy692 ∉ (SemanticCore.Class.cv nb078AlphaDummy650).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy649).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_831 :

nb078AlphaDummy691 ≠ nb078AlphaDummy692

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_832 (g : SemanticCore.Var) :

nb078AlphaDummy657 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy651 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy652 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_833 (g : SemanticCore.Var) :

nb078AlphaDummy658 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy651 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy652 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_834 (g : SemanticCore.Var) :

nb078AlphaDummy657 g ≠ nb078AlphaDummy658 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_835 (g : SemanticCore.Var) :

nb078AlphaDummy693 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy652 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy651 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_836 (g : SemanticCore.Var) :

nb078AlphaDummy694 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy652 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy651 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_837 (g : SemanticCore.Var) :

nb078AlphaDummy693 g ≠ nb078AlphaDummy694 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_838 :

nb078AlphaDummy663 ∉ (SemanticCore.Class.cv nb078AlphaDummy656).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_839 :

nb078AlphaDummy664 ∉ (SemanticCore.Class.cv nb078AlphaDummy656).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_840 :

nb078AlphaDummy663 ≠ nb078AlphaDummy664

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_841 (g : SemanticCore.Var) :

nb078AlphaDummy665 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy658 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_842 (g : SemanticCore.Var) :

nb078AlphaDummy666 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy658 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_843 (g : SemanticCore.Var) :

nb078AlphaDummy665 g ≠ nb078AlphaDummy666 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_844 :

nb078AlphaDummy669 ∉ (SemanticCore.Class.cv nb078AlphaDummy663).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_845 :

nb078AlphaDummy670 ∉ (SemanticCore.Class.cv nb078AlphaDummy663).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_846 :

nb078AlphaDummy671 ∉ (SemanticCore.Class.cv nb078AlphaDummy663).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_847 :

nb078AlphaDummy669 ≠ nb078AlphaDummy670

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_848 :

nb078AlphaDummy669 ≠ nb078AlphaDummy671

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_849 :

nb078AlphaDummy670 ≠ nb078AlphaDummy671

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_850 (g : SemanticCore.Var) :

nb078AlphaDummy672 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy665 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_851 (g : SemanticCore.Var) :

nb078AlphaDummy673 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy665 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_852 (g : SemanticCore.Var) :

nb078AlphaDummy674 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy665 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_853 (g : SemanticCore.Var) :

nb078AlphaDummy672 g ≠ nb078AlphaDummy673 g

Certificates from NAR4C078C001Part016.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_854 (g : SemanticCore.Var) :

nb078AlphaDummy672 g ≠ nb078AlphaDummy674 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_855 (g : SemanticCore.Var) :

nb078AlphaDummy673 g ≠ nb078AlphaDummy674 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_856 :

nb078AlphaDummy681 ∉ (SemanticCore.Class.cv nb078AlphaDummy670).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy670).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_857 :

nb078AlphaDummy677 ∉ (SemanticCore.Class.cv nb078AlphaDummy670).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy671).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_858 :

nb078AlphaDummy683 ∉ (SemanticCore.Class.cv nb078AlphaDummy671).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy671).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_859 (g : SemanticCore.Var) :

nb078AlphaDummy682 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy673 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy673 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_860 (g : SemanticCore.Var) :

nb078AlphaDummy678 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy673 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy674 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_861 (g : SemanticCore.Var) :

nb078AlphaDummy684 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy674 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy674 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_862 :

nb078AlphaDummy699 ∉ (SemanticCore.Class.cv nb078AlphaDummy692).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_863 :

nb078AlphaDummy700 ∉ (SemanticCore.Class.cv nb078AlphaDummy692).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_864 :

nb078AlphaDummy699 ≠ nb078AlphaDummy700

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_865 (g : SemanticCore.Var) :

nb078AlphaDummy701 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy694 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_866 (g : SemanticCore.Var) :

nb078AlphaDummy702 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy694 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_867 (g : SemanticCore.Var) :

nb078AlphaDummy701 g ≠ nb078AlphaDummy702 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_868 :

nb078AlphaDummy705 ∉ (SemanticCore.Class.cv nb078AlphaDummy699).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_869 :

nb078AlphaDummy706 ∉ (SemanticCore.Class.cv nb078AlphaDummy699).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_870 :

nb078AlphaDummy707 ∉ (SemanticCore.Class.cv nb078AlphaDummy699).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_871 :

nb078AlphaDummy705 ≠ nb078AlphaDummy706

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_872 :

nb078AlphaDummy705 ≠ nb078AlphaDummy707

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_873 :

nb078AlphaDummy706 ≠ nb078AlphaDummy707

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_874 (g : SemanticCore.Var) :

nb078AlphaDummy708 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy701 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_875 (g : SemanticCore.Var) :

nb078AlphaDummy709 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy701 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_876 (g : SemanticCore.Var) :

nb078AlphaDummy710 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy701 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_877 (g : SemanticCore.Var) :

nb078AlphaDummy708 g ≠ nb078AlphaDummy709 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_878 (g : SemanticCore.Var) :

nb078AlphaDummy708 g ≠ nb078AlphaDummy710 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_879 (g : SemanticCore.Var) :

nb078AlphaDummy709 g ≠ nb078AlphaDummy710 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_880 :

nb078AlphaDummy717 ∉ (SemanticCore.Class.cv nb078AlphaDummy706).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy706).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_881 :

nb078AlphaDummy713 ∉ (SemanticCore.Class.cv nb078AlphaDummy706).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy707).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_882 :

nb078AlphaDummy719 ∉ (SemanticCore.Class.cv nb078AlphaDummy707).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy707).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_883 (g : SemanticCore.Var) :

nb078AlphaDummy718 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy709 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy709 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_884 (g : SemanticCore.Var) :

nb078AlphaDummy714 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy709 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy710 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_885 (g : SemanticCore.Var) :

nb078AlphaDummy720 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy710 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy710 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_886 :

nb078AlphaDummy735 ∉ (SemanticCore.Class.cv nb078AlphaDummy728).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_887 :

nb078AlphaDummy736 ∉ (SemanticCore.Class.cv nb078AlphaDummy728).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_888 :

nb078AlphaDummy735 ≠ nb078AlphaDummy736

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_889 (g : SemanticCore.Var) :

nb078AlphaDummy737 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy730 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_890 (g : SemanticCore.Var) :

nb078AlphaDummy738 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy730 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_891 (g : SemanticCore.Var) :

nb078AlphaDummy737 g ≠ nb078AlphaDummy738 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_892 :

nb078AlphaDummy741 ∉ (SemanticCore.Class.cv nb078AlphaDummy735).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_893 :

nb078AlphaDummy742 ∉ (SemanticCore.Class.cv nb078AlphaDummy735).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_894 :

nb078AlphaDummy743 ∉ (SemanticCore.Class.cv nb078AlphaDummy735).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_895 :

nb078AlphaDummy741 ≠ nb078AlphaDummy742

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_896 :

nb078AlphaDummy741 ≠ nb078AlphaDummy743

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_897 :

nb078AlphaDummy742 ≠ nb078AlphaDummy743

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_898 (g : SemanticCore.Var) :

nb078AlphaDummy744 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy737 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_899 (g : SemanticCore.Var) :

nb078AlphaDummy745 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy737 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_900 (g : SemanticCore.Var) :

nb078AlphaDummy746 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy737 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_901 (g : SemanticCore.Var) :

nb078AlphaDummy744 g ≠ nb078AlphaDummy745 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_902 (g : SemanticCore.Var) :

nb078AlphaDummy744 g ≠ nb078AlphaDummy746 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_903 (g : SemanticCore.Var) :

nb078AlphaDummy745 g ≠ nb078AlphaDummy746 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_904 :

nb078AlphaDummy753 ∉ (SemanticCore.Class.cv nb078AlphaDummy742).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy742).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_905 :

nb078AlphaDummy749 ∉ (SemanticCore.Class.cv nb078AlphaDummy742).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy743).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_906 :

nb078AlphaDummy755 ∉ (SemanticCore.Class.cv nb078AlphaDummy743).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy743).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_907 (g : SemanticCore.Var) :

nb078AlphaDummy754 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy745 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy745 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_908 (g : SemanticCore.Var) :

nb078AlphaDummy750 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy745 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy746 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_909 (g : SemanticCore.Var) :

nb078AlphaDummy756 g ∉ (SemanticCore.Class.cv (nb078AlphaDummy746 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy746 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_910 :

nb078AlphaDummy775 ∉ (SemanticCore.Class.cv nb078AlphaDummy767).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy768).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_911 :

nb078AlphaDummy776 ∉ (SemanticCore.Class.cv nb078AlphaDummy767).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy768).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_912 :

nb078AlphaDummy775 ≠ nb078AlphaDummy776

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_913 :

nb078AlphaDummy811 ∉ (SemanticCore.Class.cv nb078AlphaDummy767).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy769).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_914 :

nb078AlphaDummy812 ∉ (SemanticCore.Class.cv nb078AlphaDummy767).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy769).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_915 :

nb078AlphaDummy811 ≠ nb078AlphaDummy812

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_916 :

nb078AlphaDummy925 ∉ (SemanticCore.Class.cv nb078AlphaDummy769).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy768).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_917 :

nb078AlphaDummy926 ∉ (SemanticCore.Class.cv nb078AlphaDummy769).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy768).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_918 :

nb078AlphaDummy925 ≠ nb078AlphaDummy926

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_919 (h : SemanticCore.Var) :

nb078AlphaDummy777 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy770 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy771 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_920 (h : SemanticCore.Var) :

nb078AlphaDummy778 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy770 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy771 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_921 (h : SemanticCore.Var) :

nb078AlphaDummy777 h ≠ nb078AlphaDummy778 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_922 (h : SemanticCore.Var) :

nb078AlphaDummy813 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy770 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy772 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_923 (h : SemanticCore.Var) :

nb078AlphaDummy814 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy770 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy772 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_924 (h : SemanticCore.Var) :

nb078AlphaDummy813 h ≠ nb078AlphaDummy814 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_925 (h : SemanticCore.Var) :

nb078AlphaDummy927 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy772 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy771 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_926 (h : SemanticCore.Var) :

nb078AlphaDummy928 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy772 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy771 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_927 (h : SemanticCore.Var) :

nb078AlphaDummy927 h ≠ nb078AlphaDummy928 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_928 :

nb078AlphaDummy783 ∉ (SemanticCore.Class.cv nb078AlphaDummy776).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_929 :

nb078AlphaDummy784 ∉ (SemanticCore.Class.cv nb078AlphaDummy776).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_930 :

nb078AlphaDummy783 ≠ nb078AlphaDummy784

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_931 (h : SemanticCore.Var) :

nb078AlphaDummy785 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy778 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_932 (h : SemanticCore.Var) :

nb078AlphaDummy786 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy778 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_933 (h : SemanticCore.Var) :

nb078AlphaDummy785 h ≠ nb078AlphaDummy786 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_934 :

nb078AlphaDummy789 ∉ (SemanticCore.Class.cv nb078AlphaDummy783).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_935 :

nb078AlphaDummy790 ∉ (SemanticCore.Class.cv nb078AlphaDummy783).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_936 :

nb078AlphaDummy791 ∉ (SemanticCore.Class.cv nb078AlphaDummy783).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_937 :

nb078AlphaDummy789 ≠ nb078AlphaDummy790

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_938 :

nb078AlphaDummy789 ≠ nb078AlphaDummy791

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_939 :

nb078AlphaDummy790 ≠ nb078AlphaDummy791

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_940 (h : SemanticCore.Var) :

nb078AlphaDummy792 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy785 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_941 (h : SemanticCore.Var) :

nb078AlphaDummy793 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy785 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_942 (h : SemanticCore.Var) :

nb078AlphaDummy794 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy785 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_943 (h : SemanticCore.Var) :

nb078AlphaDummy792 h ≠ nb078AlphaDummy793 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_944 (h : SemanticCore.Var) :

nb078AlphaDummy792 h ≠ nb078AlphaDummy794 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_945 (h : SemanticCore.Var) :

nb078AlphaDummy793 h ≠ nb078AlphaDummy794 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_946 :

nb078AlphaDummy801 ∉ (SemanticCore.Class.cv nb078AlphaDummy790).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy790).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_947 :

nb078AlphaDummy797 ∉ (SemanticCore.Class.cv nb078AlphaDummy790).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy791).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_948 :

nb078AlphaDummy803 ∉ (SemanticCore.Class.cv nb078AlphaDummy791).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy791).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_949 (h : SemanticCore.Var) :

nb078AlphaDummy802 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy793 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy793 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_950 (h : SemanticCore.Var) :

nb078AlphaDummy798 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy793 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy794 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_951 (h : SemanticCore.Var) :

nb078AlphaDummy804 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy794 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy794 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_952 :

nb078AlphaDummy819 ∉ (SemanticCore.Class.cv nb078AlphaDummy812).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_953 :

nb078AlphaDummy820 ∉ (SemanticCore.Class.cv nb078AlphaDummy812).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_954 :

nb078AlphaDummy819 ≠ nb078AlphaDummy820

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_955 (h : SemanticCore.Var) :

nb078AlphaDummy821 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy814 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_956 (h : SemanticCore.Var) :

nb078AlphaDummy822 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy814 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_957 (h : SemanticCore.Var) :

nb078AlphaDummy821 h ≠ nb078AlphaDummy822 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_958 :

nb078AlphaDummy825 ∉ (SemanticCore.Class.cv nb078AlphaDummy819).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_959 :

nb078AlphaDummy826 ∉ (SemanticCore.Class.cv nb078AlphaDummy819).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_960 :

nb078AlphaDummy827 ∉ (SemanticCore.Class.cv nb078AlphaDummy819).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_961 :

nb078AlphaDummy825 ≠ nb078AlphaDummy826

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_962 :

nb078AlphaDummy825 ≠ nb078AlphaDummy827

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_963 :

nb078AlphaDummy826 ≠ nb078AlphaDummy827

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_964 (h : SemanticCore.Var) :

nb078AlphaDummy828 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy821 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_965 (h : SemanticCore.Var) :

nb078AlphaDummy829 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy821 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_966 (h : SemanticCore.Var) :

nb078AlphaDummy830 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy821 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_967 (h : SemanticCore.Var) :

nb078AlphaDummy828 h ≠ nb078AlphaDummy829 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_968 (h : SemanticCore.Var) :

nb078AlphaDummy828 h ≠ nb078AlphaDummy830 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_969 (h : SemanticCore.Var) :

nb078AlphaDummy829 h ≠ nb078AlphaDummy830 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_970 :

nb078AlphaDummy837 ∉ (SemanticCore.Class.cv nb078AlphaDummy826).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy826).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_971 :

nb078AlphaDummy833 ∉ (SemanticCore.Class.cv nb078AlphaDummy826).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy827).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_972 :

nb078AlphaDummy839 ∉ (SemanticCore.Class.cv nb078AlphaDummy827).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy827).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_973 (h : SemanticCore.Var) :

nb078AlphaDummy838 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy829 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy829 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_974 (h : SemanticCore.Var) :

nb078AlphaDummy834 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy829 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy830 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_975 (h : SemanticCore.Var) :

nb078AlphaDummy840 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy830 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy830 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_976 :

nb078AlphaDummy853 ∉ (SemanticCore.Class.cv nb078AlphaDummy847).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy848).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_977 :

nb078AlphaDummy854 ∉ (SemanticCore.Class.cv nb078AlphaDummy847).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy848).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_978 :

nb078AlphaDummy853 ≠ nb078AlphaDummy854

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_979 :

nb078AlphaDummy889 ∉ (SemanticCore.Class.cv nb078AlphaDummy848).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy847).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_980 :

nb078AlphaDummy890 ∉ (SemanticCore.Class.cv nb078AlphaDummy848).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy847).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_981 :

nb078AlphaDummy889 ≠ nb078AlphaDummy890

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_982 (h : SemanticCore.Var) :

nb078AlphaDummy855 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy849 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy850 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_983 (h : SemanticCore.Var) :

nb078AlphaDummy856 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy849 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy850 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_984 (h : SemanticCore.Var) :

nb078AlphaDummy855 h ≠ nb078AlphaDummy856 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_985 (h : SemanticCore.Var) :

nb078AlphaDummy891 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy850 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy849 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_986 (h : SemanticCore.Var) :

nb078AlphaDummy892 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy850 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy849 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_987 (h : SemanticCore.Var) :

nb078AlphaDummy891 h ≠ nb078AlphaDummy892 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_988 :

nb078AlphaDummy861 ∉ (SemanticCore.Class.cv nb078AlphaDummy854).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_989 :

nb078AlphaDummy862 ∉ (SemanticCore.Class.cv nb078AlphaDummy854).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_990 :

nb078AlphaDummy861 ≠ nb078AlphaDummy862

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_991 (h : SemanticCore.Var) :

nb078AlphaDummy863 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy856 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_992 (h : SemanticCore.Var) :

nb078AlphaDummy864 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy856 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_993 (h : SemanticCore.Var) :

nb078AlphaDummy863 h ≠ nb078AlphaDummy864 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_994 :

nb078AlphaDummy867 ∉ (SemanticCore.Class.cv nb078AlphaDummy861).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_995 :

nb078AlphaDummy868 ∉ (SemanticCore.Class.cv nb078AlphaDummy861).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_996 :

nb078AlphaDummy869 ∉ (SemanticCore.Class.cv nb078AlphaDummy861).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_997 :

nb078AlphaDummy867 ≠ nb078AlphaDummy868

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_998 :

nb078AlphaDummy867 ≠ nb078AlphaDummy869

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_999 :

nb078AlphaDummy868 ≠ nb078AlphaDummy869

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1000 (h : SemanticCore.Var) :

nb078AlphaDummy870 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy863 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1001 (h : SemanticCore.Var) :

nb078AlphaDummy871 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy863 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1002 (h : SemanticCore.Var) :

nb078AlphaDummy872 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy863 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1003 (h : SemanticCore.Var) :

nb078AlphaDummy870 h ≠ nb078AlphaDummy871 h

Certificates from NAR4C078C001Part017.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1004 (h : SemanticCore.Var) :

nb078AlphaDummy870 h ≠ nb078AlphaDummy872 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1005 (h : SemanticCore.Var) :

nb078AlphaDummy871 h ≠ nb078AlphaDummy872 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1006 :

nb078AlphaDummy879 ∉ (SemanticCore.Class.cv nb078AlphaDummy868).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy868).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1007 :

nb078AlphaDummy875 ∉ (SemanticCore.Class.cv nb078AlphaDummy868).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy869).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1008 :

nb078AlphaDummy881 ∉ (SemanticCore.Class.cv nb078AlphaDummy869).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy869).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1009 (h : SemanticCore.Var) :

nb078AlphaDummy880 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy871 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy871 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1010 (h : SemanticCore.Var) :

nb078AlphaDummy876 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy871 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy872 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1011 (h : SemanticCore.Var) :

nb078AlphaDummy882 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy872 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy872 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1012 :

nb078AlphaDummy897 ∉ (SemanticCore.Class.cv nb078AlphaDummy890).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1013 :

nb078AlphaDummy898 ∉ (SemanticCore.Class.cv nb078AlphaDummy890).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1014 :

nb078AlphaDummy897 ≠ nb078AlphaDummy898

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1015 (h : SemanticCore.Var) :

nb078AlphaDummy899 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy892 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1016 (h : SemanticCore.Var) :

nb078AlphaDummy900 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy892 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1017 (h : SemanticCore.Var) :

nb078AlphaDummy899 h ≠ nb078AlphaDummy900 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1018 :

nb078AlphaDummy903 ∉ (SemanticCore.Class.cv nb078AlphaDummy897).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1019 :

nb078AlphaDummy904 ∉ (SemanticCore.Class.cv nb078AlphaDummy897).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1020 :

nb078AlphaDummy905 ∉ (SemanticCore.Class.cv nb078AlphaDummy897).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1021 :

nb078AlphaDummy903 ≠ nb078AlphaDummy904

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1022 :

nb078AlphaDummy903 ≠ nb078AlphaDummy905

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1023 :

nb078AlphaDummy904 ≠ nb078AlphaDummy905

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1024 (h : SemanticCore.Var) :

nb078AlphaDummy906 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy899 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1025 (h : SemanticCore.Var) :

nb078AlphaDummy907 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy899 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1026 (h : SemanticCore.Var) :

nb078AlphaDummy908 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy899 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1027 (h : SemanticCore.Var) :

nb078AlphaDummy906 h ≠ nb078AlphaDummy907 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1028 (h : SemanticCore.Var) :

nb078AlphaDummy906 h ≠ nb078AlphaDummy908 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1029 (h : SemanticCore.Var) :

nb078AlphaDummy907 h ≠ nb078AlphaDummy908 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1030 :

nb078AlphaDummy915 ∉ (SemanticCore.Class.cv nb078AlphaDummy904).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy904).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1031 :

nb078AlphaDummy911 ∉ (SemanticCore.Class.cv nb078AlphaDummy904).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy905).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1032 :

nb078AlphaDummy917 ∉ (SemanticCore.Class.cv nb078AlphaDummy905).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy905).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1033 (h : SemanticCore.Var) :

nb078AlphaDummy916 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy907 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy907 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1034 (h : SemanticCore.Var) :

nb078AlphaDummy912 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy907 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy908 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1035 (h : SemanticCore.Var) :

nb078AlphaDummy918 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy908 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy908 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1036 :

nb078AlphaDummy933 ∉ (SemanticCore.Class.cv nb078AlphaDummy926).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1037 :

nb078AlphaDummy934 ∉ (SemanticCore.Class.cv nb078AlphaDummy926).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1038 :

nb078AlphaDummy933 ≠ nb078AlphaDummy934

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1039 (h : SemanticCore.Var) :

nb078AlphaDummy935 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy928 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1040 (h : SemanticCore.Var) :

nb078AlphaDummy936 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy928 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1041 (h : SemanticCore.Var) :

nb078AlphaDummy935 h ≠ nb078AlphaDummy936 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1042 :

nb078AlphaDummy939 ∉ (SemanticCore.Class.cv nb078AlphaDummy933).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1043 :

nb078AlphaDummy940 ∉ (SemanticCore.Class.cv nb078AlphaDummy933).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1044 :

nb078AlphaDummy941 ∉ (SemanticCore.Class.cv nb078AlphaDummy933).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1045 :

nb078AlphaDummy939 ≠ nb078AlphaDummy940

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1046 :

nb078AlphaDummy939 ≠ nb078AlphaDummy941

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1047 :

nb078AlphaDummy940 ≠ nb078AlphaDummy941

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1048 (h : SemanticCore.Var) :

nb078AlphaDummy942 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy935 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1049 (h : SemanticCore.Var) :

nb078AlphaDummy943 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy935 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1050 (h : SemanticCore.Var) :

nb078AlphaDummy944 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy935 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1051 (h : SemanticCore.Var) :

nb078AlphaDummy942 h ≠ nb078AlphaDummy943 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1052 (h : SemanticCore.Var) :

nb078AlphaDummy942 h ≠ nb078AlphaDummy944 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1053 (h : SemanticCore.Var) :

nb078AlphaDummy943 h ≠ nb078AlphaDummy944 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1054 :

nb078AlphaDummy951 ∉ (SemanticCore.Class.cv nb078AlphaDummy940).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy940).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1055 :

nb078AlphaDummy947 ∉ (SemanticCore.Class.cv nb078AlphaDummy940).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy941).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1056 :

nb078AlphaDummy953 ∉ (SemanticCore.Class.cv nb078AlphaDummy941).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy941).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1057 (h : SemanticCore.Var) :

nb078AlphaDummy952 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy943 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy943 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1058 (h : SemanticCore.Var) :

nb078AlphaDummy948 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy943 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy944 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1059 (h : SemanticCore.Var) :

nb078AlphaDummy954 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy944 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy944 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1060 :

nb078AlphaDummy965 ∉ (SemanticCore.Class.cv nb078AlphaDummy962).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy961).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1061 :

nb078AlphaDummy966 ∉ (SemanticCore.Class.cv nb078AlphaDummy962).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy961).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1062 :

nb078AlphaDummy965 ≠ nb078AlphaDummy966

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1063 (h : SemanticCore.Var) :

nb078AlphaDummy967 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy964 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy963 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1064 (h : SemanticCore.Var) :

nb078AlphaDummy968 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy964 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy963 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1065 (h : SemanticCore.Var) :

nb078AlphaDummy967 h ≠ nb078AlphaDummy968 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1066 :

nb078AlphaDummy973 ∉ (SemanticCore.Class.cv nb078AlphaDummy966).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1067 :

nb078AlphaDummy974 ∉ (SemanticCore.Class.cv nb078AlphaDummy966).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1068 :

nb078AlphaDummy973 ≠ nb078AlphaDummy974

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1069 (h : SemanticCore.Var) :

nb078AlphaDummy975 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy968 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1070 (h : SemanticCore.Var) :

nb078AlphaDummy976 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy968 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1071 (h : SemanticCore.Var) :

nb078AlphaDummy975 h ≠ nb078AlphaDummy976 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1072 :

nb078AlphaDummy979 ∉ (SemanticCore.Class.cv nb078AlphaDummy973).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1073 :

nb078AlphaDummy980 ∉ (SemanticCore.Class.cv nb078AlphaDummy973).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1074 :

nb078AlphaDummy981 ∉ (SemanticCore.Class.cv nb078AlphaDummy973).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1075 :

nb078AlphaDummy979 ≠ nb078AlphaDummy980

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1076 :

nb078AlphaDummy979 ≠ nb078AlphaDummy981

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1077 :

nb078AlphaDummy980 ≠ nb078AlphaDummy981

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1078 (h : SemanticCore.Var) :

nb078AlphaDummy982 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy975 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1079 (h : SemanticCore.Var) :

nb078AlphaDummy983 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy975 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1080 (h : SemanticCore.Var) :

nb078AlphaDummy984 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy975 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1081 (h : SemanticCore.Var) :

nb078AlphaDummy982 h ≠ nb078AlphaDummy983 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1082 (h : SemanticCore.Var) :

nb078AlphaDummy982 h ≠ nb078AlphaDummy984 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1083 (h : SemanticCore.Var) :

nb078AlphaDummy983 h ≠ nb078AlphaDummy984 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1084 :

nb078AlphaDummy991 ∉ (SemanticCore.Class.cv nb078AlphaDummy980).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy980).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1085 :

nb078AlphaDummy987 ∉ (SemanticCore.Class.cv nb078AlphaDummy980).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy981).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1086 :

nb078AlphaDummy993 ∉ (SemanticCore.Class.cv nb078AlphaDummy981).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy981).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1087 (h : SemanticCore.Var) :

nb078AlphaDummy992 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy983 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy983 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1088 (h : SemanticCore.Var) :

nb078AlphaDummy988 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy983 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy984 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1089 (h : SemanticCore.Var) :

nb078AlphaDummy994 h ∉ (SemanticCore.Class.cv (nb078AlphaDummy984 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy984 h)).fv

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

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

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

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

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

nb078AlphaDummy091 f ≠ nb078AlphaDummy092 f

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

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

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

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

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

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

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

nb078AlphaDummy012 f ≠ nb078AlphaDummy013 f

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

nb078AlphaDummy012 f ≠ nb078AlphaDummy014 f

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

nb078AlphaDummy013 f ≠ nb078AlphaDummy014 f

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

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

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

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

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

nb078AlphaDummy245 f ≠ nb078AlphaDummy246 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1102 (g : SemanticCore.Var) :

nb078AlphaDummy369 g ∉ (SemanticCore.Class.cv g).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1103 (g : SemanticCore.Var) :

nb078AlphaDummy370 g ∉ (SemanticCore.Class.cv g).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1104 (g : SemanticCore.Var) :

nb078AlphaDummy369 g ≠ nb078AlphaDummy370 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1105 (g : SemanticCore.Var) :

nb078AlphaDummy290 g ∉ (SemanticCore.Class.cv g).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1106 (g : SemanticCore.Var) :

nb078AlphaDummy291 g ∉ (SemanticCore.Class.cv g).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1107 (g : SemanticCore.Var) :

nb078AlphaDummy292 g ∉ (SemanticCore.Class.cv g).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1108 (g : SemanticCore.Var) :

nb078AlphaDummy290 g ≠ nb078AlphaDummy291 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1109 (g : SemanticCore.Var) :

nb078AlphaDummy290 g ≠ nb078AlphaDummy292 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1110 (g : SemanticCore.Var) :

nb078AlphaDummy291 g ≠ nb078AlphaDummy292 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1111 (g : SemanticCore.Var) :

nb078AlphaDummy527 g ∉ (SemanticCore.Class.cv g).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1112 (g : SemanticCore.Var) :

nb078AlphaDummy528 g ∉ (SemanticCore.Class.cv g).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1113 (g : SemanticCore.Var) :

nb078AlphaDummy527 g ≠ nb078AlphaDummy528 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1114 (h : SemanticCore.Var) :

nb078AlphaDummy849 h ∉ (SemanticCore.Class.cv h).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1115 (h : SemanticCore.Var) :

nb078AlphaDummy850 h ∉ (SemanticCore.Class.cv h).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1116 (h : SemanticCore.Var) :

nb078AlphaDummy849 h ≠ nb078AlphaDummy850 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1117 (h : SemanticCore.Var) :

nb078AlphaDummy770 h ∉ (SemanticCore.Class.cv h).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1118 (h : SemanticCore.Var) :

nb078AlphaDummy771 h ∉ (SemanticCore.Class.cv h).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1119 (h : SemanticCore.Var) :

nb078AlphaDummy772 h ∉ (SemanticCore.Class.cv h).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1120 (h : SemanticCore.Var) :

nb078AlphaDummy770 h ≠ nb078AlphaDummy771 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1121 (h : SemanticCore.Var) :

nb078AlphaDummy770 h ≠ nb078AlphaDummy772 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1122 (h : SemanticCore.Var) :

nb078AlphaDummy771 h ≠ nb078AlphaDummy772 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1123 (h : SemanticCore.Var) :

nb078AlphaDummy1007 h ∉ (SemanticCore.Class.cv h).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1124 (h : SemanticCore.Var) :

nb078AlphaDummy1008 h ∉ (SemanticCore.Class.cv h).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1125 (h : SemanticCore.Var) :

nb078AlphaDummy1007 h ≠ nb078AlphaDummy1008 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1126 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1128 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1130 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1131 (h : SemanticCore.Var) :

nb078AlphaDummy1022 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy1019 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy1019 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1019 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1132 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1134 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1135 (h : SemanticCore.Var) :

nb078AlphaDummy1070 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy1067 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy1067 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1067 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1136 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1137 (h : SemanticCore.Var) :

nb078AlphaDummy1106 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy1103 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy1103 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1103 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1138 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1139 (h : SemanticCore.Var) :

nb078AlphaDummy1148 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy1145 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy1145 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1145 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1140 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1141 (h : SemanticCore.Var) :

nb078AlphaDummy1184 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy1181 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy1181 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1181 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1142 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1143 (h : SemanticCore.Var) :

nb078AlphaDummy1220 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy1217 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy1217 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1217 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1144 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1146 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1148 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1150 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1152 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1153 (g : SemanticCore.Var) :

nb078AlphaDummy308 g ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy305 g)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy305 g)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy305 g)).fv