Nominal proof certificates grouped in dependency order.

Certificates from NAR4C078C001Part018.

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

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

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

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

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

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

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

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1166 : nb078AlphaDummy589 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy585) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy585) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy585).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1167 (g : SemanticCore.Var) : nb078AlphaDummy590 g ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy587 g)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy587 g)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy587 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1168 : nb078AlphaDummy625 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy621) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy621) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy621).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1169 (g : SemanticCore.Var) : nb078AlphaDummy626 g ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy623 g)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy623 g)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy623 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1170 : nb078AlphaDummy667 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy663) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy663) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy663).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1171 (g : SemanticCore.Var) : nb078AlphaDummy668 g ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy665 g)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy665 g)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy665 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1172 : nb078AlphaDummy703 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy699) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy699) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy699).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1173 (g : SemanticCore.Var) : nb078AlphaDummy704 g ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy701 g)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy701 g)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy701 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1174 : nb078AlphaDummy739 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy735) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy735) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy735).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1175 (g : SemanticCore.Var) : nb078AlphaDummy740 g ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy737 g)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy737 g)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy737 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1176 : nb078AlphaDummy787 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy783) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy783) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy783).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1177 (h : SemanticCore.Var) : nb078AlphaDummy788 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy785 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy785 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy785 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1178 : nb078AlphaDummy823 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy819) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy819) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy819).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1179 (h : SemanticCore.Var) : nb078AlphaDummy824 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy821 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy821 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy821 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1180 : nb078AlphaDummy865 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy861) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy861) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy861).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1181 (h : SemanticCore.Var) : nb078AlphaDummy866 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy863 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy863 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy863 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1182 : nb078AlphaDummy901 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy897) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy897) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy897).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1183 (h : SemanticCore.Var) : nb078AlphaDummy902 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy899 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy899 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy899 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1184 : nb078AlphaDummy937 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy933) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy933) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy933).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1185 (h : SemanticCore.Var) : nb078AlphaDummy938 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy935 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy935 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy935 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1186 : nb078AlphaDummy977 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy973) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy973) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy973).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1187 (h : SemanticCore.Var) : nb078AlphaDummy978 h ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy975 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy975 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy975 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1188 : nb078AlphaDummy203 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy000)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1189 : nb078AlphaDummy204 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy000)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1190 : nb078AlphaDummy203 ≠ nb078AlphaDummy204

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1191 : nb078AlphaDummy649 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1192 : nb078AlphaDummy650 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1193 : nb078AlphaDummy649 ≠ nb078AlphaDummy650

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1194 : nb078AlphaDummy569 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1195 : nb078AlphaDummy570 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1196 : nb078AlphaDummy571 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1197 : nb078AlphaDummy569 ≠ nb078AlphaDummy570

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1198 : nb078AlphaDummy569 ≠ nb078AlphaDummy571

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1199 : nb078AlphaDummy570 ≠ nb078AlphaDummy571

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1200 : nb078AlphaDummy481 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1201 : nb078AlphaDummy482 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1202 : nb078AlphaDummy481 ≠ nb078AlphaDummy482

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1203 : nb078AlphaDummy1129 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1204 : nb078AlphaDummy1130 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1205 : nb078AlphaDummy1129 ≠ nb078AlphaDummy1130

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1206 : nb078AlphaDummy1049 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1207 : nb078AlphaDummy1050 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1208 : nb078AlphaDummy1051 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1209 : nb078AlphaDummy1049 ≠ nb078AlphaDummy1050

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1210 : nb078AlphaDummy1049 ≠ nb078AlphaDummy1051

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1211 : nb078AlphaDummy1050 ≠ nb078AlphaDummy1051

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1212 : nb078AlphaDummy961 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1213 : nb078AlphaDummy962 ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1214 : nb078AlphaDummy961 ≠ nb078AlphaDummy962

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1215 (f : SemanticCore.Var) : nb078AlphaDummy205 f ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1216 (f : SemanticCore.Var) : nb078AlphaDummy206 f ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1217 (f : SemanticCore.Var) : nb078AlphaDummy205 f ≠ nb078AlphaDummy206 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1218 (g : SemanticCore.Var) : nb078AlphaDummy651 g ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1219 (g : SemanticCore.Var) : nb078AlphaDummy652 g ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1220 (g : SemanticCore.Var) : nb078AlphaDummy651 g ≠ nb078AlphaDummy652 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1221 (g : SemanticCore.Var) : nb078AlphaDummy572 g ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1222 (g : SemanticCore.Var) : nb078AlphaDummy573 g ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1223 (g : SemanticCore.Var) : nb078AlphaDummy574 g ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1224 (g : SemanticCore.Var) : nb078AlphaDummy572 g ≠ nb078AlphaDummy573 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1225 (g : SemanticCore.Var) : nb078AlphaDummy572 g ≠ nb078AlphaDummy574 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1226 (g : SemanticCore.Var) : nb078AlphaDummy573 g ≠ nb078AlphaDummy574 g

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1227 (g : SemanticCore.Var) : nb078AlphaDummy483 g ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1228 (g : SemanticCore.Var) : nb078AlphaDummy484 g ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1229 (g : SemanticCore.Var) : nb078AlphaDummy483 g ≠ nb078AlphaDummy484 g

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1232 (h : SemanticCore.Var) : nb078AlphaDummy1131 h ≠ nb078AlphaDummy1132 h

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1236 (h : SemanticCore.Var) : nb078AlphaDummy1052 h ≠ nb078AlphaDummy1053 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1237 (h : SemanticCore.Var) : nb078AlphaDummy1052 h ≠ nb078AlphaDummy1054 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1238 (h : SemanticCore.Var) : nb078AlphaDummy1053 h ≠ nb078AlphaDummy1054 h

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1241 (h : SemanticCore.Var) : nb078AlphaDummy963 h ≠ nb078AlphaDummy964 h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1242 : nb078AlphaDummy007 ∉ (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb078AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy000))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1243 : nb078AlphaDummy285 ∉ (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb078AlphaDummy001) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1244 : nb078AlphaDummy765 ∉ (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb078AlphaDummy002) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1245 (f : SemanticCore.Var) : nb078AlphaDummy008 f ∉ (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1248 : nb078AlphaDummy567 ∉ (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1249 : nb078AlphaDummy1047 ∉ (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1252 : nb078AlphaDummy021 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy017 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy018 (SemanticCore.Class.cv nb078AlphaDummy009) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy017) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy017 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy018 (SemanticCore.Class.cv nb078AlphaDummy010) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy017) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1253 (f : SemanticCore.Var) : nb078AlphaDummy022 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy019 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy020 f) (SemanticCore.Class.cv (nb078AlphaDummy012 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy019 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy019 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy020 f) (SemanticCore.Class.cv (nb078AlphaDummy013 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy019 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1254 : nb078AlphaDummy057 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy054 (SemanticCore.Class.cv nb078AlphaDummy009) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy053) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy054 (SemanticCore.Class.cv nb078AlphaDummy011) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1255 (f : SemanticCore.Var) : nb078AlphaDummy058 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy056 f) (SemanticCore.Class.cv (nb078AlphaDummy012 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy056 f) (SemanticCore.Class.cv (nb078AlphaDummy014 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1256 : nb078AlphaDummy099 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy095 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy096 (SemanticCore.Class.cv nb078AlphaDummy089) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy095) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy095 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy096 (SemanticCore.Class.cv nb078AlphaDummy090) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy095) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1257 (f : SemanticCore.Var) : nb078AlphaDummy100 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy097 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy098 f) (SemanticCore.Class.cv (nb078AlphaDummy091 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy097 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy097 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy098 f) (SemanticCore.Class.cv (nb078AlphaDummy092 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy097 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1258 : nb078AlphaDummy1013 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1009 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1010 (SemanticCore.Class.cv nb078AlphaDummy1006) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1009) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1009 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1010 (SemanticCore.Class.cv nb078AlphaDummy1005) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1009) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1259 (h : SemanticCore.Var) : nb078AlphaDummy1014 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1011 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1012 h) (SemanticCore.Class.cv (nb078AlphaDummy1008 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1011 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1011 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1012 h) (SemanticCore.Class.cv (nb078AlphaDummy1007 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1011 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1260 : nb078AlphaDummy1061 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1057 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1058 (SemanticCore.Class.cv nb078AlphaDummy1049) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1057) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1057 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1058 (SemanticCore.Class.cv nb078AlphaDummy1050) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1057) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1261 (h : SemanticCore.Var) : nb078AlphaDummy1062 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1059 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1060 h) (SemanticCore.Class.cv (nb078AlphaDummy1052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1059 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1059 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1060 h) (SemanticCore.Class.cv (nb078AlphaDummy1053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1059 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1262 : nb078AlphaDummy1097 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1093 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1094 (SemanticCore.Class.cv nb078AlphaDummy1049) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1093) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1094)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1093 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1094 (SemanticCore.Class.cv nb078AlphaDummy1051) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1093) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1094)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1263 (h : SemanticCore.Var) : nb078AlphaDummy1098 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1095 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1096 h) (SemanticCore.Class.cv (nb078AlphaDummy1052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1095 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1096 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1095 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1096 h) (SemanticCore.Class.cv (nb078AlphaDummy1054 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1095 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1096 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1264 : nb078AlphaDummy1139 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1135 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1136 (SemanticCore.Class.cv nb078AlphaDummy1129) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1135) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1136)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1135 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1136 (SemanticCore.Class.cv nb078AlphaDummy1130) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1135) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1136)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1265 (h : SemanticCore.Var) : nb078AlphaDummy1140 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1137 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1138 h) (SemanticCore.Class.cv (nb078AlphaDummy1131 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1137 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1138 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1137 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1138 h) (SemanticCore.Class.cv (nb078AlphaDummy1132 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1137 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1138 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1266 : nb078AlphaDummy1175 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1171 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1172 (SemanticCore.Class.cv nb078AlphaDummy1130) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1171) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1172)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1171 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1172 (SemanticCore.Class.cv nb078AlphaDummy1129) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1171) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1172)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1267 (h : SemanticCore.Var) : nb078AlphaDummy1176 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1173 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1174 h) (SemanticCore.Class.cv (nb078AlphaDummy1132 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1173 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1174 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1173 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1174 h) (SemanticCore.Class.cv (nb078AlphaDummy1131 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1173 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1174 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1268 : nb078AlphaDummy1211 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1207 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1208 (SemanticCore.Class.cv nb078AlphaDummy1051) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1207) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1208)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1207 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1208 (SemanticCore.Class.cv nb078AlphaDummy1050) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1207) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1208)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1269 (h : SemanticCore.Var) : nb078AlphaDummy1212 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1209 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1210 h) (SemanticCore.Class.cv (nb078AlphaDummy1054 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1209 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1210 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1209 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1210 h) (SemanticCore.Class.cv (nb078AlphaDummy1053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1209 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1210 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1270 : nb078AlphaDummy135 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy132 (SemanticCore.Class.cv nb078AlphaDummy090) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy131) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy132 (SemanticCore.Class.cv nb078AlphaDummy089) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1271 (f : SemanticCore.Var) : nb078AlphaDummy136 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy134 f) (SemanticCore.Class.cv (nb078AlphaDummy092 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy134 f) (SemanticCore.Class.cv (nb078AlphaDummy091 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1272 : nb078AlphaDummy171 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy168 (SemanticCore.Class.cv nb078AlphaDummy011) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy167) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy168 (SemanticCore.Class.cv nb078AlphaDummy010) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1273 (f : SemanticCore.Var) : nb078AlphaDummy172 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy170 f) (SemanticCore.Class.cv (nb078AlphaDummy014 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy170 f) (SemanticCore.Class.cv (nb078AlphaDummy013 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

Certificates from NAR4C078C001Part019.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1274 : nb078AlphaDummy211 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy207 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy208 (SemanticCore.Class.cv nb078AlphaDummy204) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy207) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy207 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy208 (SemanticCore.Class.cv nb078AlphaDummy203) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy207) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1275 (f : SemanticCore.Var) : nb078AlphaDummy212 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy209 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy210 f) (SemanticCore.Class.cv (nb078AlphaDummy206 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy209 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy209 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy210 f) (SemanticCore.Class.cv (nb078AlphaDummy205 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy209 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1276 : nb078AlphaDummy251 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy247 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy248 (SemanticCore.Class.cv nb078AlphaDummy244) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy247) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy247 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy248 (SemanticCore.Class.cv nb078AlphaDummy243) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy247) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1277 (f : SemanticCore.Var) : nb078AlphaDummy252 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy249 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy250 f) (SemanticCore.Class.cv (nb078AlphaDummy246 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy249 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy249 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy250 f) (SemanticCore.Class.cv (nb078AlphaDummy245 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy249 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1294 : nb078AlphaDummy617 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy613 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy614 (SemanticCore.Class.cv nb078AlphaDummy569) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy613) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy613 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy614 (SemanticCore.Class.cv nb078AlphaDummy571) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy613) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1295 (g : SemanticCore.Var) : nb078AlphaDummy618 g ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy615 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy616 g) (SemanticCore.Class.cv (nb078AlphaDummy572 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy615 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy615 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy616 g) (SemanticCore.Class.cv (nb078AlphaDummy574 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy615 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1296 : nb078AlphaDummy659 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy655 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy656 (SemanticCore.Class.cv nb078AlphaDummy649) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy655) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy656)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy655 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy656 (SemanticCore.Class.cv nb078AlphaDummy650) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy655) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy656)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1297 (g : SemanticCore.Var) : nb078AlphaDummy660 g ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy657 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy658 g) (SemanticCore.Class.cv (nb078AlphaDummy651 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy657 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy658 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy657 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy658 g) (SemanticCore.Class.cv (nb078AlphaDummy652 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy657 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy658 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1298 : nb078AlphaDummy695 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy691 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy692 (SemanticCore.Class.cv nb078AlphaDummy650) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy691) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy692)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy691 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy692 (SemanticCore.Class.cv nb078AlphaDummy649) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy691) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy692)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1299 (g : SemanticCore.Var) : nb078AlphaDummy696 g ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy693 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy694 g) (SemanticCore.Class.cv (nb078AlphaDummy652 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy693 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy694 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy693 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy694 g) (SemanticCore.Class.cv (nb078AlphaDummy651 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy693 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy694 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1300 : nb078AlphaDummy731 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy727 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy728 (SemanticCore.Class.cv nb078AlphaDummy571) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy727) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy728)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy727 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy728 (SemanticCore.Class.cv nb078AlphaDummy570) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy727) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy728)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1301 (g : SemanticCore.Var) : nb078AlphaDummy732 g ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy729 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy730 g) (SemanticCore.Class.cv (nb078AlphaDummy574 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy729 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy730 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy729 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy730 g) (SemanticCore.Class.cv (nb078AlphaDummy573 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy729 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy730 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1302 : nb078AlphaDummy779 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy775 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy776 (SemanticCore.Class.cv nb078AlphaDummy767) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy775) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy775 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy776 (SemanticCore.Class.cv nb078AlphaDummy768) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy775) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1303 (h : SemanticCore.Var) : nb078AlphaDummy780 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy777 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy778 h) (SemanticCore.Class.cv (nb078AlphaDummy770 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy777 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy777 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy778 h) (SemanticCore.Class.cv (nb078AlphaDummy771 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy777 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1304 : nb078AlphaDummy815 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy811 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy812 (SemanticCore.Class.cv nb078AlphaDummy767) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy811) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy811 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy812 (SemanticCore.Class.cv nb078AlphaDummy769) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy811) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1305 (h : SemanticCore.Var) : nb078AlphaDummy816 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy813 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy814 h) (SemanticCore.Class.cv (nb078AlphaDummy770 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy813 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy813 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy814 h) (SemanticCore.Class.cv (nb078AlphaDummy772 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy813 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1306 : nb078AlphaDummy857 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy853 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy854 (SemanticCore.Class.cv nb078AlphaDummy847) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy853) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy853 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy854 (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy853) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1307 (h : SemanticCore.Var) : nb078AlphaDummy858 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy855 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy856 h) (SemanticCore.Class.cv (nb078AlphaDummy849 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy855 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy855 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy856 h) (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy855 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1308 : nb078AlphaDummy893 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy889 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy890 (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy889) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy889 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy890 (SemanticCore.Class.cv nb078AlphaDummy847) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy889) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1309 (h : SemanticCore.Var) : nb078AlphaDummy894 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy891 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy892 h) (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy891 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy891 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy892 h) (SemanticCore.Class.cv (nb078AlphaDummy849 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy891 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1310 : nb078AlphaDummy929 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy925 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy926 (SemanticCore.Class.cv nb078AlphaDummy769) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy925) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy925 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy926 (SemanticCore.Class.cv nb078AlphaDummy768) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy925) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1311 (h : SemanticCore.Var) : nb078AlphaDummy930 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy927 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy928 h) (SemanticCore.Class.cv (nb078AlphaDummy772 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy927 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy927 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy928 h) (SemanticCore.Class.cv (nb078AlphaDummy771 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy927 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1312 : nb078AlphaDummy969 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy965 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy966 (SemanticCore.Class.cv nb078AlphaDummy962) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy965) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy965 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy966 (SemanticCore.Class.cv nb078AlphaDummy961) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy965) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1313 (h : SemanticCore.Var) : nb078AlphaDummy970 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy967 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy968 h) (SemanticCore.Class.cv (nb078AlphaDummy964 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy967 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy967 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy968 h) (SemanticCore.Class.cv (nb078AlphaDummy963 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy967 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1314 : nb078AlphaDummy041 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy032)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy033)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1315 (f : SemanticCore.Var) : nb078AlphaDummy042 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy035 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy036 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1316 : nb078AlphaDummy077 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy068)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy069)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1317 (f : SemanticCore.Var) : nb078AlphaDummy078 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy071 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy072 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1318 : nb078AlphaDummy1033 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1024)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1025)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1319 (h : SemanticCore.Var) : nb078AlphaDummy1034 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1027 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1028 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1320 : nb078AlphaDummy1081 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1072)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1073)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1321 (h : SemanticCore.Var) : nb078AlphaDummy1082 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1075 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1076 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1322 : nb078AlphaDummy119 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy110)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy111)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1323 : nb078AlphaDummy1117 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1108)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1109)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1324 (h : SemanticCore.Var) : nb078AlphaDummy1118 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1111 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1112 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1325 (f : SemanticCore.Var) : nb078AlphaDummy120 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy113 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy114 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1326 : nb078AlphaDummy1159 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1150)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1151)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1327 (h : SemanticCore.Var) : nb078AlphaDummy1160 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1153 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1154 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1328 : nb078AlphaDummy1195 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1186)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1187)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1329 (h : SemanticCore.Var) : nb078AlphaDummy1196 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1189 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1190 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1330 : nb078AlphaDummy1231 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1222)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1223)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1331 (h : SemanticCore.Var) : nb078AlphaDummy1232 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1225 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1226 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1332 : nb078AlphaDummy155 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy146)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy147)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1333 (f : SemanticCore.Var) : nb078AlphaDummy156 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy149 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy150 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1334 : nb078AlphaDummy191 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy182)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy183)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1335 (f : SemanticCore.Var) : nb078AlphaDummy192 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy185 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy186 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1336 : nb078AlphaDummy231 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy222)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy223)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1337 (f : SemanticCore.Var) : nb078AlphaDummy232 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy225 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy226 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1338 : nb078AlphaDummy271 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy262)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy263)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1339 (f : SemanticCore.Var) : nb078AlphaDummy272 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy265 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy266 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1340 : nb078AlphaDummy319 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy310)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy311)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1342 : nb078AlphaDummy355 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy346)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy347)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1344 : nb078AlphaDummy397 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy388)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy389)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1346 : nb078AlphaDummy433 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy424)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy425)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1348 : nb078AlphaDummy469 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy460)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy461)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1350 : nb078AlphaDummy509 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy500)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy501)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1352 : nb078AlphaDummy553 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy544)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy545)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1354 : nb078AlphaDummy601 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy592)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy593)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1355 (g : SemanticCore.Var) : nb078AlphaDummy602 g ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy595 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy596 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1356 : nb078AlphaDummy637 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy628)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy629)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1357 (g : SemanticCore.Var) : nb078AlphaDummy638 g ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy631 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy632 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1358 : nb078AlphaDummy679 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy670)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy671)).fv

Certificates from NAR4C078C001Part020.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1359 (g : SemanticCore.Var) : nb078AlphaDummy680 g ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy673 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy674 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1360 : nb078AlphaDummy715 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy706)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy707)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1361 (g : SemanticCore.Var) : nb078AlphaDummy716 g ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy709 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy710 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1362 : nb078AlphaDummy751 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy742)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy743)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1363 (g : SemanticCore.Var) : nb078AlphaDummy752 g ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy745 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy746 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1364 : nb078AlphaDummy799 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy790)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy791)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1365 (h : SemanticCore.Var) : nb078AlphaDummy800 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy793 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy794 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1366 : nb078AlphaDummy835 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy826)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy827)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1367 (h : SemanticCore.Var) : nb078AlphaDummy836 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy829 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy830 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1368 : nb078AlphaDummy877 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy868)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy869)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1369 (h : SemanticCore.Var) : nb078AlphaDummy878 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy871 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy872 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1370 : nb078AlphaDummy913 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy904)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy905)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1371 (h : SemanticCore.Var) : nb078AlphaDummy914 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy907 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy908 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1372 : nb078AlphaDummy949 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy940)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy941)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1373 (h : SemanticCore.Var) : nb078AlphaDummy950 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy943 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy944 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1374 : nb078AlphaDummy989 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy980)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy981)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1375 (h : SemanticCore.Var) : nb078AlphaDummy990 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy983 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy984 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1376 : nb078AlphaDummy049 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1377 (f : SemanticCore.Var) : nb078AlphaDummy050 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1378 : nb078AlphaDummy085 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1379 (f : SemanticCore.Var) : nb078AlphaDummy086 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1380 : nb078AlphaDummy127 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1381 (f : SemanticCore.Var) : nb078AlphaDummy128 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1382 : nb078AlphaDummy1041 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1383 (h : SemanticCore.Var) : nb078AlphaDummy1042 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1384 : nb078AlphaDummy1089 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1385 (h : SemanticCore.Var) : nb078AlphaDummy1090 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1386 : nb078AlphaDummy1125 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1094))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1387 (h : SemanticCore.Var) : nb078AlphaDummy1126 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1096 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1388 : nb078AlphaDummy1167 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1136))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1389 (h : SemanticCore.Var) : nb078AlphaDummy1168 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1138 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1390 : nb078AlphaDummy1203 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1172))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1391 (h : SemanticCore.Var) : nb078AlphaDummy1204 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1174 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1392 : nb078AlphaDummy1239 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1208))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1393 (h : SemanticCore.Var) : nb078AlphaDummy1240 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1210 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1394 : nb078AlphaDummy163 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1395 (f : SemanticCore.Var) : nb078AlphaDummy164 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1396 : nb078AlphaDummy199 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1397 (f : SemanticCore.Var) : nb078AlphaDummy200 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1398 : nb078AlphaDummy239 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1399 (f : SemanticCore.Var) : nb078AlphaDummy240 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1400 : nb078AlphaDummy279 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1401 (f : SemanticCore.Var) : nb078AlphaDummy280 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1416 : nb078AlphaDummy609 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy578))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1417 (g : SemanticCore.Var) : nb078AlphaDummy610 g ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy580 g)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1418 : nb078AlphaDummy645 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1419 (g : SemanticCore.Var) : nb078AlphaDummy646 g ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1420 : nb078AlphaDummy687 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy656))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1421 (g : SemanticCore.Var) : nb078AlphaDummy688 g ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy658 g)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1422 : nb078AlphaDummy723 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy692))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1423 (g : SemanticCore.Var) : nb078AlphaDummy724 g ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy694 g)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1424 : nb078AlphaDummy759 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy728))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1425 (g : SemanticCore.Var) : nb078AlphaDummy760 g ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy730 g)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1426 : nb078AlphaDummy807 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1427 (h : SemanticCore.Var) : nb078AlphaDummy808 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1428 : nb078AlphaDummy843 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1429 (h : SemanticCore.Var) : nb078AlphaDummy844 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1430 : nb078AlphaDummy885 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1431 (h : SemanticCore.Var) : nb078AlphaDummy886 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1432 : nb078AlphaDummy921 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1433 (h : SemanticCore.Var) : nb078AlphaDummy922 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1434 : nb078AlphaDummy957 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1435 (h : SemanticCore.Var) : nb078AlphaDummy958 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1436 : nb078AlphaDummy997 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1437 (h : SemanticCore.Var) : nb078AlphaDummy998 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1438 : nb078AlphaDummy037 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy032) (SemanticCore.Class.cv nb078AlphaDummy033)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy032) (SemanticCore.Class.cv nb078AlphaDummy033)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1439 (f : SemanticCore.Var) : nb078AlphaDummy038 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy035 f)) (SemanticCore.Class.cv (nb078AlphaDummy036 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy035 f)) (SemanticCore.Class.cv (nb078AlphaDummy036 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1440 : nb078AlphaDummy073 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy068) (SemanticCore.Class.cv nb078AlphaDummy069)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy068) (SemanticCore.Class.cv nb078AlphaDummy069)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1441 (f : SemanticCore.Var) : nb078AlphaDummy074 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy071 f)) (SemanticCore.Class.cv (nb078AlphaDummy072 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy071 f)) (SemanticCore.Class.cv (nb078AlphaDummy072 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1442 : nb078AlphaDummy1029 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1024) (SemanticCore.Class.cv nb078AlphaDummy1025)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1024) (SemanticCore.Class.cv nb078AlphaDummy1025)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1443 (h : SemanticCore.Var) : nb078AlphaDummy1030 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1027 h)) (SemanticCore.Class.cv (nb078AlphaDummy1028 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1027 h)) (SemanticCore.Class.cv (nb078AlphaDummy1028 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1444 : nb078AlphaDummy1077 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1072) (SemanticCore.Class.cv nb078AlphaDummy1073)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1072) (SemanticCore.Class.cv nb078AlphaDummy1073)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1445 (h : SemanticCore.Var) : nb078AlphaDummy1078 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1075 h)) (SemanticCore.Class.cv (nb078AlphaDummy1076 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1075 h)) (SemanticCore.Class.cv (nb078AlphaDummy1076 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1446 : nb078AlphaDummy115 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy110) (SemanticCore.Class.cv nb078AlphaDummy111)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy110) (SemanticCore.Class.cv nb078AlphaDummy111)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1447 : nb078AlphaDummy1113 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1108) (SemanticCore.Class.cv nb078AlphaDummy1109)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1108) (SemanticCore.Class.cv nb078AlphaDummy1109)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1448 (h : SemanticCore.Var) : nb078AlphaDummy1114 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1111 h)) (SemanticCore.Class.cv (nb078AlphaDummy1112 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1111 h)) (SemanticCore.Class.cv (nb078AlphaDummy1112 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1449 (f : SemanticCore.Var) : nb078AlphaDummy116 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy113 f)) (SemanticCore.Class.cv (nb078AlphaDummy114 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy113 f)) (SemanticCore.Class.cv (nb078AlphaDummy114 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1450 : nb078AlphaDummy1155 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1150) (SemanticCore.Class.cv nb078AlphaDummy1151)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1150) (SemanticCore.Class.cv nb078AlphaDummy1151)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1451 (h : SemanticCore.Var) : nb078AlphaDummy1156 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1153 h)) (SemanticCore.Class.cv (nb078AlphaDummy1154 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1153 h)) (SemanticCore.Class.cv (nb078AlphaDummy1154 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1452 : nb078AlphaDummy1191 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1186) (SemanticCore.Class.cv nb078AlphaDummy1187)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1186) (SemanticCore.Class.cv nb078AlphaDummy1187)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1453 (h : SemanticCore.Var) : nb078AlphaDummy1192 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1189 h)) (SemanticCore.Class.cv (nb078AlphaDummy1190 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1189 h)) (SemanticCore.Class.cv (nb078AlphaDummy1190 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1454 : nb078AlphaDummy1227 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1222) (SemanticCore.Class.cv nb078AlphaDummy1223)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1222) (SemanticCore.Class.cv nb078AlphaDummy1223)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1455 (h : SemanticCore.Var) : nb078AlphaDummy1228 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1225 h)) (SemanticCore.Class.cv (nb078AlphaDummy1226 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1225 h)) (SemanticCore.Class.cv (nb078AlphaDummy1226 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1456 : nb078AlphaDummy151 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy146) (SemanticCore.Class.cv nb078AlphaDummy147)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy146) (SemanticCore.Class.cv nb078AlphaDummy147)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1457 (f : SemanticCore.Var) : nb078AlphaDummy152 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy149 f)) (SemanticCore.Class.cv (nb078AlphaDummy150 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy149 f)) (SemanticCore.Class.cv (nb078AlphaDummy150 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1458 : nb078AlphaDummy187 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy182) (SemanticCore.Class.cv nb078AlphaDummy183)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy182) (SemanticCore.Class.cv nb078AlphaDummy183)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1459 (f : SemanticCore.Var) : nb078AlphaDummy188 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy185 f)) (SemanticCore.Class.cv (nb078AlphaDummy186 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy185 f)) (SemanticCore.Class.cv (nb078AlphaDummy186 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1460 : nb078AlphaDummy227 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy222) (SemanticCore.Class.cv nb078AlphaDummy223)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy222) (SemanticCore.Class.cv nb078AlphaDummy223)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1461 (f : SemanticCore.Var) : nb078AlphaDummy228 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy225 f)) (SemanticCore.Class.cv (nb078AlphaDummy226 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy225 f)) (SemanticCore.Class.cv (nb078AlphaDummy226 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1462 : nb078AlphaDummy267 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy262) (SemanticCore.Class.cv nb078AlphaDummy263)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy262) (SemanticCore.Class.cv nb078AlphaDummy263)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1463 (f : SemanticCore.Var) : nb078AlphaDummy268 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy265 f)) (SemanticCore.Class.cv (nb078AlphaDummy266 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy265 f)) (SemanticCore.Class.cv (nb078AlphaDummy266 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1464 : nb078AlphaDummy315 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy310) (SemanticCore.Class.cv nb078AlphaDummy311)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy310) (SemanticCore.Class.cv nb078AlphaDummy311)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1465 (g : SemanticCore.Var) : nb078AlphaDummy316 g ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy313 g)) (SemanticCore.Class.cv (nb078AlphaDummy314 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy313 g)) (SemanticCore.Class.cv (nb078AlphaDummy314 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1466 : nb078AlphaDummy351 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy346) (SemanticCore.Class.cv nb078AlphaDummy347)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy346) (SemanticCore.Class.cv nb078AlphaDummy347)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1468 : nb078AlphaDummy393 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy388) (SemanticCore.Class.cv nb078AlphaDummy389)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy388) (SemanticCore.Class.cv nb078AlphaDummy389)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1470 : nb078AlphaDummy429 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy424) (SemanticCore.Class.cv nb078AlphaDummy425)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy424) (SemanticCore.Class.cv nb078AlphaDummy425)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1472 : nb078AlphaDummy465 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy460) (SemanticCore.Class.cv nb078AlphaDummy461)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy460) (SemanticCore.Class.cv nb078AlphaDummy461)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1474 : nb078AlphaDummy505 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy500) (SemanticCore.Class.cv nb078AlphaDummy501)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy500) (SemanticCore.Class.cv nb078AlphaDummy501)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1476 : nb078AlphaDummy549 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy544) (SemanticCore.Class.cv nb078AlphaDummy545)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy544) (SemanticCore.Class.cv nb078AlphaDummy545)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1478 : nb078AlphaDummy597 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy592) (SemanticCore.Class.cv nb078AlphaDummy593)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy592) (SemanticCore.Class.cv nb078AlphaDummy593)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1479 (g : SemanticCore.Var) : nb078AlphaDummy598 g ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy595 g)) (SemanticCore.Class.cv (nb078AlphaDummy596 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy595 g)) (SemanticCore.Class.cv (nb078AlphaDummy596 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1480 : nb078AlphaDummy633 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy628) (SemanticCore.Class.cv nb078AlphaDummy629)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy628) (SemanticCore.Class.cv nb078AlphaDummy629)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1481 (g : SemanticCore.Var) : nb078AlphaDummy634 g ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy631 g)) (SemanticCore.Class.cv (nb078AlphaDummy632 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy631 g)) (SemanticCore.Class.cv (nb078AlphaDummy632 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1482 : nb078AlphaDummy675 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy670) (SemanticCore.Class.cv nb078AlphaDummy671)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy670) (SemanticCore.Class.cv nb078AlphaDummy671)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1483 (g : SemanticCore.Var) : nb078AlphaDummy676 g ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy673 g)) (SemanticCore.Class.cv (nb078AlphaDummy674 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy673 g)) (SemanticCore.Class.cv (nb078AlphaDummy674 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1484 : nb078AlphaDummy711 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy706) (SemanticCore.Class.cv nb078AlphaDummy707)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy706) (SemanticCore.Class.cv nb078AlphaDummy707)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1485 (g : SemanticCore.Var) : nb078AlphaDummy712 g ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy709 g)) (SemanticCore.Class.cv (nb078AlphaDummy710 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy709 g)) (SemanticCore.Class.cv (nb078AlphaDummy710 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1486 : nb078AlphaDummy747 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy742) (SemanticCore.Class.cv nb078AlphaDummy743)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy742) (SemanticCore.Class.cv nb078AlphaDummy743)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1487 (g : SemanticCore.Var) : nb078AlphaDummy748 g ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy745 g)) (SemanticCore.Class.cv (nb078AlphaDummy746 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy745 g)) (SemanticCore.Class.cv (nb078AlphaDummy746 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1488 : nb078AlphaDummy795 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy790) (SemanticCore.Class.cv nb078AlphaDummy791)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy790) (SemanticCore.Class.cv nb078AlphaDummy791)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1489 (h : SemanticCore.Var) : nb078AlphaDummy796 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy793 h)) (SemanticCore.Class.cv (nb078AlphaDummy794 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy793 h)) (SemanticCore.Class.cv (nb078AlphaDummy794 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1490 : nb078AlphaDummy831 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy826) (SemanticCore.Class.cv nb078AlphaDummy827)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy826) (SemanticCore.Class.cv nb078AlphaDummy827)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1491 (h : SemanticCore.Var) : nb078AlphaDummy832 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy829 h)) (SemanticCore.Class.cv (nb078AlphaDummy830 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy829 h)) (SemanticCore.Class.cv (nb078AlphaDummy830 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1492 : nb078AlphaDummy873 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy868) (SemanticCore.Class.cv nb078AlphaDummy869)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy868) (SemanticCore.Class.cv nb078AlphaDummy869)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1493 (h : SemanticCore.Var) : nb078AlphaDummy874 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy871 h)) (SemanticCore.Class.cv (nb078AlphaDummy872 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy871 h)) (SemanticCore.Class.cv (nb078AlphaDummy872 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1494 : nb078AlphaDummy909 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy904) (SemanticCore.Class.cv nb078AlphaDummy905)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy904) (SemanticCore.Class.cv nb078AlphaDummy905)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1495 (h : SemanticCore.Var) : nb078AlphaDummy910 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy907 h)) (SemanticCore.Class.cv (nb078AlphaDummy908 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy907 h)) (SemanticCore.Class.cv (nb078AlphaDummy908 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1496 : nb078AlphaDummy945 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy940) (SemanticCore.Class.cv nb078AlphaDummy941)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy940) (SemanticCore.Class.cv nb078AlphaDummy941)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1497 (h : SemanticCore.Var) : nb078AlphaDummy946 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy943 h)) (SemanticCore.Class.cv (nb078AlphaDummy944 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy943 h)) (SemanticCore.Class.cv (nb078AlphaDummy944 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1498 : nb078AlphaDummy985 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy980) (SemanticCore.Class.cv nb078AlphaDummy981)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy980) (SemanticCore.Class.cv nb078AlphaDummy981)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1499 (h : SemanticCore.Var) : nb078AlphaDummy986 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy983 h)) (SemanticCore.Class.cv (nb078AlphaDummy984 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy983 h)) (SemanticCore.Class.cv (nb078AlphaDummy984 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1500 : nb078AlphaDummy005 ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb078AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy000))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb078AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy000))) Compiler.CompactSourceSyntax.synCid).fv

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

Certificates from NAR4C078C001Part021.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1502 : nb078AlphaDummy763 ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb078AlphaDummy002) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb078AlphaDummy002) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002))) Compiler.CompactSourceSyntax.synCid).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1503 (f : SemanticCore.Var) : nb078AlphaDummy006 f ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid).fv

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1507 : nb078AlphaDummy1045 ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)))) Compiler.CompactSourceSyntax.synCid).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1510 : nb078AlphaDummy521 ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy001)) (SemanticCore.Class.cv nb078AlphaDummy003)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy001)) (SemanticCore.Class.cv nb078AlphaDummy003)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1511 : nb078AlphaDummy1001 ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy002)) (SemanticCore.Class.cv nb078AlphaDummy004)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy002)) (SemanticCore.Class.cv nb078AlphaDummy004)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1513 (y h : SemanticCore.Var) : nb078AlphaDummy1002 y h ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)) (SemanticCore.Class.cv y)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)) (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1514 : nb078AlphaDummy051 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1515 (f : SemanticCore.Var) : nb078AlphaDummy052 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1516 : nb078AlphaDummy087 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1517 (f : SemanticCore.Var) : nb078AlphaDummy088 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1518 : nb078AlphaDummy129 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1519 (f : SemanticCore.Var) : nb078AlphaDummy130 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1520 : nb078AlphaDummy1043 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1521 (h : SemanticCore.Var) : nb078AlphaDummy1044 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1522 : nb078AlphaDummy1091 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1523 (h : SemanticCore.Var) : nb078AlphaDummy1092 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1524 : nb078AlphaDummy1127 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1094)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1094)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1525 (h : SemanticCore.Var) : nb078AlphaDummy1128 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1096 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1096 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1526 : nb078AlphaDummy1169 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1136)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1136)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1527 (h : SemanticCore.Var) : nb078AlphaDummy1170 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1138 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1138 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1528 : nb078AlphaDummy1205 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1172)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1172)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1529 (h : SemanticCore.Var) : nb078AlphaDummy1206 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1174 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1174 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1530 : nb078AlphaDummy1241 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1208)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1208)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1531 (h : SemanticCore.Var) : nb078AlphaDummy1242 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1210 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1210 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1532 : nb078AlphaDummy165 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1533 (f : SemanticCore.Var) : nb078AlphaDummy166 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1534 : nb078AlphaDummy201 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1535 (f : SemanticCore.Var) : nb078AlphaDummy202 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1536 : nb078AlphaDummy241 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1537 (f : SemanticCore.Var) : nb078AlphaDummy242 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1538 : nb078AlphaDummy281 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1539 (f : SemanticCore.Var) : nb078AlphaDummy282 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1540 : nb078AlphaDummy329 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy296)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy296)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1541 (g : SemanticCore.Var) : nb078AlphaDummy330 g ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1542 : nb078AlphaDummy365 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy332)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy332)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1543 (g : SemanticCore.Var) : nb078AlphaDummy366 g ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1544 : nb078AlphaDummy407 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy374)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy374)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1545 (g : SemanticCore.Var) : nb078AlphaDummy408 g ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy376 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1546 : nb078AlphaDummy443 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy410)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy410)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1547 (g : SemanticCore.Var) : nb078AlphaDummy444 g ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy412 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1548 : nb078AlphaDummy479 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy446)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy446)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1549 (g : SemanticCore.Var) : nb078AlphaDummy480 g ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy448 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1550 : nb078AlphaDummy519 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy486)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy486)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1551 (g : SemanticCore.Var) : nb078AlphaDummy520 g ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy488 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1552 : nb078AlphaDummy563 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy530)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy530)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1553 (g : SemanticCore.Var) : nb078AlphaDummy564 g ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy532 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1554 : nb078AlphaDummy611 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy578)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy578)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1555 (g : SemanticCore.Var) : nb078AlphaDummy612 g ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy580 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy580 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1556 : nb078AlphaDummy647 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1557 (g : SemanticCore.Var) : nb078AlphaDummy648 g ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1558 : nb078AlphaDummy689 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy656)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy656)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1559 (g : SemanticCore.Var) : nb078AlphaDummy690 g ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy658 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy658 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1560 : nb078AlphaDummy725 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy692)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy692)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1561 (g : SemanticCore.Var) : nb078AlphaDummy726 g ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy694 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy694 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1562 : nb078AlphaDummy761 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy728)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy728)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1563 (g : SemanticCore.Var) : nb078AlphaDummy762 g ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy730 g))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy730 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1564 : nb078AlphaDummy809 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1565 (h : SemanticCore.Var) : nb078AlphaDummy810 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1566 : nb078AlphaDummy845 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1567 (h : SemanticCore.Var) : nb078AlphaDummy846 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1568 : nb078AlphaDummy887 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1569 (h : SemanticCore.Var) : nb078AlphaDummy888 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1570 : nb078AlphaDummy923 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1571 (h : SemanticCore.Var) : nb078AlphaDummy924 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1572 : nb078AlphaDummy959 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1573 (h : SemanticCore.Var) : nb078AlphaDummy960 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1574 : nb078AlphaDummy999 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1575 (h : SemanticCore.Var) : nb078AlphaDummy1000 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1576 : nb078AlphaDummy523 ∉ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy001)).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy003).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1577 : nb078AlphaDummy1003 ∉ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy002)).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy004).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1578 (x g : SemanticCore.Var) : nb078AlphaDummy524 x g ∉ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv g)).fv ∪ (SemanticCore.Class.cv x).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1579 (y h : SemanticCore.Var) : nb078AlphaDummy1004 y h ∉ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1580 : nb078AlphaDummy015 ∉ {nb078AlphaDummy009} ∪ {nb078AlphaDummy010} ∪ (Compiler.CompactSourceSyntax.synWex nb078AlphaDummy011 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy009) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy000)) (SemanticCore.Class.cv nb078AlphaDummy011)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy011) (SemanticCore.Class.cv nb078AlphaDummy000) (SemanticCore.Class.cv nb078AlphaDummy010)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1581 (f : SemanticCore.Var) : nb078AlphaDummy016 f ∉ {nb078AlphaDummy012 f} ∪ {nb078AlphaDummy013 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb078AlphaDummy014 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy012 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb078AlphaDummy014 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy014 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb078AlphaDummy013 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1582 : nb078AlphaDummy093 ∉ {nb078AlphaDummy089} ∪ {nb078AlphaDummy090} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy090) (SemanticCore.Class.cv nb078AlphaDummy000) (SemanticCore.Class.cv nb078AlphaDummy089)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1583 (f : SemanticCore.Var) : nb078AlphaDummy094 f ∉ {nb078AlphaDummy091 f} ∪ {nb078AlphaDummy092 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy092 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb078AlphaDummy091 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1584 : nb078AlphaDummy1055 ∉ {nb078AlphaDummy1049} ∪ {nb078AlphaDummy1050} ∪ (Compiler.CompactSourceSyntax.synWex nb078AlphaDummy1051 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy1049) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002))) (SemanticCore.Class.cv nb078AlphaDummy1051)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy1051) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)) (SemanticCore.Class.cv nb078AlphaDummy1050)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1585 (h : SemanticCore.Var) : nb078AlphaDummy1056 h ∉ {nb078AlphaDummy1052 h} ∪ {nb078AlphaDummy1053 h} ∪ (Compiler.CompactSourceSyntax.synWex (nb078AlphaDummy1054 h) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy1052 h)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h))) (SemanticCore.Class.cv (nb078AlphaDummy1054 h))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy1054 h)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (SemanticCore.Class.cv (nb078AlphaDummy1053 h))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1586 : nb078AlphaDummy1133 ∉ {nb078AlphaDummy1129} ∪ {nb078AlphaDummy1130} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy1130) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)) (SemanticCore.Class.cv nb078AlphaDummy1129)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1587 (h : SemanticCore.Var) : nb078AlphaDummy1134 h ∉ {nb078AlphaDummy1131 h} ∪ {nb078AlphaDummy1132 h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy1132 h)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (SemanticCore.Class.cv (nb078AlphaDummy1131 h))).fv

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

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1594 : nb078AlphaDummy653 ∉ {nb078AlphaDummy649} ∪ {nb078AlphaDummy650} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy650) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)) (SemanticCore.Class.cv nb078AlphaDummy649)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1595 (g : SemanticCore.Var) : nb078AlphaDummy654 g ∉ {nb078AlphaDummy651 g} ∪ {nb078AlphaDummy652 g} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy652 g)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)) (SemanticCore.Class.cv (nb078AlphaDummy651 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1596 : nb078AlphaDummy773 ∉ {nb078AlphaDummy767} ∪ {nb078AlphaDummy768} ∪ (Compiler.CompactSourceSyntax.synWex nb078AlphaDummy769 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy767) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)) (SemanticCore.Class.cv nb078AlphaDummy769)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy769) (SemanticCore.Class.cv nb078AlphaDummy002) (SemanticCore.Class.cv nb078AlphaDummy768)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1597 (h : SemanticCore.Var) : nb078AlphaDummy774 h ∉ {nb078AlphaDummy770 h} ∪ {nb078AlphaDummy771 h} ∪ (Compiler.CompactSourceSyntax.synWex (nb078AlphaDummy772 h) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy770 h)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (SemanticCore.Class.cv (nb078AlphaDummy772 h))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy772 h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb078AlphaDummy771 h))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1598 : nb078AlphaDummy851 ∉ {nb078AlphaDummy847} ∪ {nb078AlphaDummy848} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Class.cv nb078AlphaDummy002) (SemanticCore.Class.cv nb078AlphaDummy847)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1599 (h : SemanticCore.Var) : nb078AlphaDummy852 h ∉ {nb078AlphaDummy849 h} ∪ {nb078AlphaDummy850 h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb078AlphaDummy849 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1600 : nb078AlphaDummy000 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1601 : nb078AlphaDummy001 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1602 : nb078AlphaDummy002 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1603 : nb078AlphaDummy003 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_fresh_1604 : nb078AlphaDummy004 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1605 : nb078AlphaDummy000 ≠ nb078AlphaDummy001

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1606 : nb078AlphaDummy000 ≠ nb078AlphaDummy002

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1607 : nb078AlphaDummy000 ≠ nb078AlphaDummy003

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1608 : nb078AlphaDummy000 ≠ nb078AlphaDummy004

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1609 : nb078AlphaDummy001 ≠ nb078AlphaDummy002

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1610 : nb078AlphaDummy001 ≠ nb078AlphaDummy003

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1611 : nb078AlphaDummy001 ≠ nb078AlphaDummy004

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1612 : nb078AlphaDummy002 ≠ nb078AlphaDummy003

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1613 : nb078AlphaDummy002 ≠ nb078AlphaDummy004

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_distinct_1614 : nb078AlphaDummy003 ≠ nb078AlphaDummy004

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0000 : nb078AlphaDummy009 ∈ {nb078AlphaDummy009} ∪ {nb078AlphaDummy010} ∪ (Compiler.CompactSourceSyntax.synWex nb078AlphaDummy011 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy009) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy000)) (SemanticCore.Class.cv nb078AlphaDummy011)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy011) (SemanticCore.Class.cv nb078AlphaDummy000) (SemanticCore.Class.cv nb078AlphaDummy010)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0001 (f : SemanticCore.Var) : nb078AlphaDummy012 f ∈ {nb078AlphaDummy012 f} ∪ {nb078AlphaDummy013 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb078AlphaDummy014 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy012 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb078AlphaDummy014 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy014 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb078AlphaDummy013 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0002 : nb078AlphaDummy010 ∈ {nb078AlphaDummy009} ∪ {nb078AlphaDummy010} ∪ (Compiler.CompactSourceSyntax.synWex nb078AlphaDummy011 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy009) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy000)) (SemanticCore.Class.cv nb078AlphaDummy011)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy011) (SemanticCore.Class.cv nb078AlphaDummy000) (SemanticCore.Class.cv nb078AlphaDummy010)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0003 (f : SemanticCore.Var) : nb078AlphaDummy013 f ∈ {nb078AlphaDummy012 f} ∪ {nb078AlphaDummy013 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb078AlphaDummy014 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy012 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb078AlphaDummy014 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy014 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb078AlphaDummy013 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0004 : nb078AlphaDummy009 ∈ (SemanticCore.Class.cv nb078AlphaDummy009).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy010).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0005 : nb078AlphaDummy009 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy017 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy018 (SemanticCore.Class.cv nb078AlphaDummy009) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy017) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy017 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy018 (SemanticCore.Class.cv nb078AlphaDummy010) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy017) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0006 (f : SemanticCore.Var) : nb078AlphaDummy012 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy012 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy013 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0007 (f : SemanticCore.Var) : nb078AlphaDummy012 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy019 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy020 f) (SemanticCore.Class.cv (nb078AlphaDummy012 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy019 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy019 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy020 f) (SemanticCore.Class.cv (nb078AlphaDummy013 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy019 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0008 : nb078AlphaDummy009 ∈ (SemanticCore.Class.cab nb078AlphaDummy017 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy018 (SemanticCore.Class.cv nb078AlphaDummy009) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy017) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy017 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy018 (SemanticCore.Class.cv nb078AlphaDummy009) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy017) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0009 (f : SemanticCore.Var) : nb078AlphaDummy012 f ∈ (SemanticCore.Class.cab (nb078AlphaDummy019 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy020 f) (SemanticCore.Class.cv (nb078AlphaDummy012 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy019 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy019 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy020 f) (SemanticCore.Class.cv (nb078AlphaDummy012 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy019 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0010 : nb078AlphaDummy018 ∈ (SemanticCore.Class.cv nb078AlphaDummy018).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0011 (f : SemanticCore.Var) : nb078AlphaDummy020 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy020 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0012 : nb078AlphaDummy025 ∈ (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_support_mem_0013 (f : SemanticCore.Var) : nb078AlphaDummy027 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_support_mem_0014 : nb078AlphaDummy025 ∈ (SemanticCore.Class.cv nb078AlphaDummy025).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0015 (f : SemanticCore.Var) : nb078AlphaDummy027 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy027 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0016 : nb078AlphaDummy032 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy032) (SemanticCore.Class.cv nb078AlphaDummy033)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy032) (SemanticCore.Class.cv nb078AlphaDummy033)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0017 (f : SemanticCore.Var) : nb078AlphaDummy035 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy035 f)) (SemanticCore.Class.cv (nb078AlphaDummy036 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy035 f)) (SemanticCore.Class.cv (nb078AlphaDummy036 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0018 : nb078AlphaDummy032 ∈ (SemanticCore.Class.cv nb078AlphaDummy032).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy033).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0019 (f : SemanticCore.Var) : nb078AlphaDummy035 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy035 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy036 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0020 : nb078AlphaDummy033 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy032) (SemanticCore.Class.cv nb078AlphaDummy033)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy032) (SemanticCore.Class.cv nb078AlphaDummy033)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0021 (f : SemanticCore.Var) : nb078AlphaDummy036 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy035 f)) (SemanticCore.Class.cv (nb078AlphaDummy036 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy035 f)) (SemanticCore.Class.cv (nb078AlphaDummy036 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0022 : nb078AlphaDummy033 ∈ (SemanticCore.Class.cv nb078AlphaDummy032).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy033).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0023 (f : SemanticCore.Var) : nb078AlphaDummy036 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy035 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy036 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0024 : nb078AlphaDummy032 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy032)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy033)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0025 (f : SemanticCore.Var) : nb078AlphaDummy035 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy035 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy036 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0026 : nb078AlphaDummy032 ∈ (SemanticCore.Class.cv nb078AlphaDummy032).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy032).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0027 (f : SemanticCore.Var) : nb078AlphaDummy035 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy035 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy035 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0028 : nb078AlphaDummy033 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy032)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy033)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0029 (f : SemanticCore.Var) : nb078AlphaDummy036 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy035 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy036 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0030 : nb078AlphaDummy033 ∈ (SemanticCore.Class.cv nb078AlphaDummy033).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy033).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0031 (f : SemanticCore.Var) : nb078AlphaDummy036 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy036 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy036 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0032 : nb078AlphaDummy010 ∈ (SemanticCore.Class.cv nb078AlphaDummy009).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy010).fv