Nominal proof certificates grouped in dependency order.

Certificates from NAR4C078C001Part030.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1165 (h : SemanticCore.Var) : nb078AlphaDummy1112 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1112 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1112 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1166 : nb078AlphaDummy1051 ∈ (SemanticCore.Class.cv nb078AlphaDummy1049).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1051).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1167 : nb078AlphaDummy1051 ∈ (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_support_mem_1168 (h : SemanticCore.Var) : nb078AlphaDummy1054 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1052 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1054 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1169 (h : SemanticCore.Var) : nb078AlphaDummy1054 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_support_mem_1170 : nb078AlphaDummy1051 ∈ (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 ∪ (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_support_mem_1171 (h : SemanticCore.Var) : nb078AlphaDummy1054 h ∈ (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 ∪ (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_support_mem_1172 : nb078AlphaDummy1094 ∈ (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_support_mem_1173 (h : SemanticCore.Var) : nb078AlphaDummy1096 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_support_mem_1174 : nb078AlphaDummy1094 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1094)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1094)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1175 (h : SemanticCore.Var) : nb078AlphaDummy1096 h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1096 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1096 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1176 : nb078AlphaDummy1129 ∈ {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_support_mem_1177 (h : SemanticCore.Var) : nb078AlphaDummy1131 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_support_mem_1178 : nb078AlphaDummy1130 ∈ {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_support_mem_1179 (h : SemanticCore.Var) : nb078AlphaDummy1132 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_support_mem_1180 : nb078AlphaDummy1129 ∈ (SemanticCore.Class.cv nb078AlphaDummy1129).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1130).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1181 : nb078AlphaDummy1129 ∈ (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_support_mem_1182 (h : SemanticCore.Var) : nb078AlphaDummy1131 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1131 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1132 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1183 (h : SemanticCore.Var) : nb078AlphaDummy1131 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_support_mem_1184 : nb078AlphaDummy1129 ∈ (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 ∪ (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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1185 (h : SemanticCore.Var) : nb078AlphaDummy1131 h ∈ (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 ∪ (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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1186 : nb078AlphaDummy1136 ∈ (SemanticCore.Class.cv nb078AlphaDummy1136).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1187 (h : SemanticCore.Var) : nb078AlphaDummy1138 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1138 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1188 : nb078AlphaDummy1143 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy1143) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy1143) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1143).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1189 (h : SemanticCore.Var) : nb078AlphaDummy1145 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy1145 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy1145 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1145 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1190 : nb078AlphaDummy1143 ∈ (SemanticCore.Class.cv nb078AlphaDummy1143).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1191 (h : SemanticCore.Var) : nb078AlphaDummy1145 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1145 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1192 : nb078AlphaDummy1150 ∈ (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_support_mem_1193 (h : SemanticCore.Var) : nb078AlphaDummy1153 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_support_mem_1194 : nb078AlphaDummy1150 ∈ (SemanticCore.Class.cv nb078AlphaDummy1150).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1151).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1195 (h : SemanticCore.Var) : nb078AlphaDummy1153 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1153 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1154 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1196 : nb078AlphaDummy1151 ∈ (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_support_mem_1197 (h : SemanticCore.Var) : nb078AlphaDummy1154 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_support_mem_1198 : nb078AlphaDummy1151 ∈ (SemanticCore.Class.cv nb078AlphaDummy1150).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1151).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1199 (h : SemanticCore.Var) : nb078AlphaDummy1154 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1153 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1154 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1200 : nb078AlphaDummy1150 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1150)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1151)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1202 : nb078AlphaDummy1150 ∈ (SemanticCore.Class.cv nb078AlphaDummy1150).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1150).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1203 (h : SemanticCore.Var) : nb078AlphaDummy1153 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1153 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1153 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1204 : nb078AlphaDummy1151 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1150)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1151)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1206 : nb078AlphaDummy1151 ∈ (SemanticCore.Class.cv nb078AlphaDummy1151).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1151).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1207 (h : SemanticCore.Var) : nb078AlphaDummy1154 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1154 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1154 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1208 : nb078AlphaDummy1130 ∈ (SemanticCore.Class.cv nb078AlphaDummy1129).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1130).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1209 : nb078AlphaDummy1130 ∈ (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_support_mem_1210 (h : SemanticCore.Var) : nb078AlphaDummy1132 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1131 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1132 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1211 (h : SemanticCore.Var) : nb078AlphaDummy1132 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_support_mem_1212 : nb078AlphaDummy1130 ∈ (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 ∪ (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_support_mem_1213 (h : SemanticCore.Var) : nb078AlphaDummy1132 h ∈ (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 ∪ (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_support_mem_1214 : nb078AlphaDummy1136 ∈ (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_support_mem_1215 (h : SemanticCore.Var) : nb078AlphaDummy1138 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_support_mem_1216 : nb078AlphaDummy1136 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1136)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1136)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1217 (h : SemanticCore.Var) : nb078AlphaDummy1138 h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1138 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1138 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1218 : nb078AlphaDummy1130 ∈ (SemanticCore.Class.cv nb078AlphaDummy1130).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1129).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1219 : nb078AlphaDummy1130 ∈ (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_support_mem_1220 (h : SemanticCore.Var) : nb078AlphaDummy1132 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1132 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1131 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1221 (h : SemanticCore.Var) : nb078AlphaDummy1132 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_support_mem_1222 : nb078AlphaDummy1130 ∈ (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 ∪ (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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1223 (h : SemanticCore.Var) : nb078AlphaDummy1132 h ∈ (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 ∪ (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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1224 : nb078AlphaDummy1172 ∈ (SemanticCore.Class.cv nb078AlphaDummy1172).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1225 (h : SemanticCore.Var) : nb078AlphaDummy1174 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1174 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1226 : nb078AlphaDummy1179 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy1179) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy1179) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1179).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1227 (h : SemanticCore.Var) : nb078AlphaDummy1181 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy1181 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy1181 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1181 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1228 : nb078AlphaDummy1179 ∈ (SemanticCore.Class.cv nb078AlphaDummy1179).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1229 (h : SemanticCore.Var) : nb078AlphaDummy1181 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1181 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1230 : nb078AlphaDummy1186 ∈ (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_support_mem_1231 (h : SemanticCore.Var) : nb078AlphaDummy1189 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_support_mem_1232 : nb078AlphaDummy1186 ∈ (SemanticCore.Class.cv nb078AlphaDummy1186).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1187).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1233 (h : SemanticCore.Var) : nb078AlphaDummy1189 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1189 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1190 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1234 : nb078AlphaDummy1187 ∈ (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_support_mem_1235 (h : SemanticCore.Var) : nb078AlphaDummy1190 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_support_mem_1236 : nb078AlphaDummy1187 ∈ (SemanticCore.Class.cv nb078AlphaDummy1186).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1187).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1237 (h : SemanticCore.Var) : nb078AlphaDummy1190 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1189 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1190 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1238 : nb078AlphaDummy1186 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1186)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1187)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1240 : nb078AlphaDummy1186 ∈ (SemanticCore.Class.cv nb078AlphaDummy1186).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1186).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1241 (h : SemanticCore.Var) : nb078AlphaDummy1189 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1189 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1189 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1242 : nb078AlphaDummy1187 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1186)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1187)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1244 : nb078AlphaDummy1187 ∈ (SemanticCore.Class.cv nb078AlphaDummy1187).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1187).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1245 (h : SemanticCore.Var) : nb078AlphaDummy1190 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1190 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1190 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1246 : nb078AlphaDummy1129 ∈ (SemanticCore.Class.cv nb078AlphaDummy1130).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1129).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1247 : nb078AlphaDummy1129 ∈ (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_support_mem_1248 (h : SemanticCore.Var) : nb078AlphaDummy1131 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1132 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1131 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1249 (h : SemanticCore.Var) : nb078AlphaDummy1131 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_support_mem_1250 : nb078AlphaDummy1129 ∈ (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 ∪ (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_support_mem_1251 (h : SemanticCore.Var) : nb078AlphaDummy1131 h ∈ (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 ∪ (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_support_mem_1252 : nb078AlphaDummy1172 ∈ (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_support_mem_1253 (h : SemanticCore.Var) : nb078AlphaDummy1174 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_support_mem_1254 : nb078AlphaDummy1172 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1172)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1172)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1255 (h : SemanticCore.Var) : nb078AlphaDummy1174 h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1174 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1174 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1256 : nb078AlphaDummy002 ∈ (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_support_mem_1257 (h : SemanticCore.Var) : 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_support_mem_1258 : nb078AlphaDummy002 ∈ (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_support_mem_1259 (h : SemanticCore.Var) : 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_support_mem_1260 : nb078AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1261 : nb078AlphaDummy002 ∈ {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_support_mem_1262 (h : SemanticCore.Var) : 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_support_mem_1263 (h : SemanticCore.Var) : 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_support_mem_1264 : nb078AlphaDummy002 ∈ {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_support_mem_1265 (h : SemanticCore.Var) : 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_support_mem_1266 : nb078AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1267 (h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1268 : nb078AlphaDummy1051 ∈ (SemanticCore.Class.cv nb078AlphaDummy1051).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1050).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1269 : nb078AlphaDummy1051 ∈ (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_support_mem_1270 (h : SemanticCore.Var) : nb078AlphaDummy1054 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1054 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1053 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1271 (h : SemanticCore.Var) : nb078AlphaDummy1054 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_support_mem_1272 : nb078AlphaDummy1051 ∈ (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 ∪ (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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1273 (h : SemanticCore.Var) : nb078AlphaDummy1054 h ∈ (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 ∪ (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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1274 : nb078AlphaDummy1208 ∈ (SemanticCore.Class.cv nb078AlphaDummy1208).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1275 (h : SemanticCore.Var) : nb078AlphaDummy1210 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1210 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1276 : nb078AlphaDummy1215 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy1215) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy1215) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1215).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1277 (h : SemanticCore.Var) : nb078AlphaDummy1217 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy1217 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy1217 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1217 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1278 : nb078AlphaDummy1215 ∈ (SemanticCore.Class.cv nb078AlphaDummy1215).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1279 (h : SemanticCore.Var) : nb078AlphaDummy1217 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1217 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1280 : nb078AlphaDummy1222 ∈ (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_support_mem_1281 (h : SemanticCore.Var) : nb078AlphaDummy1225 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_support_mem_1282 : nb078AlphaDummy1222 ∈ (SemanticCore.Class.cv nb078AlphaDummy1222).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1223).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1283 (h : SemanticCore.Var) : nb078AlphaDummy1225 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1225 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1226 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1284 : nb078AlphaDummy1223 ∈ (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_support_mem_1285 (h : SemanticCore.Var) : nb078AlphaDummy1226 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_support_mem_1286 : nb078AlphaDummy1223 ∈ (SemanticCore.Class.cv nb078AlphaDummy1222).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1223).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1287 (h : SemanticCore.Var) : nb078AlphaDummy1226 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1225 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1226 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1288 : nb078AlphaDummy1222 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1222)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1223)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1290 : nb078AlphaDummy1222 ∈ (SemanticCore.Class.cv nb078AlphaDummy1222).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1222).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1291 (h : SemanticCore.Var) : nb078AlphaDummy1225 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1225 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1225 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1292 : nb078AlphaDummy1223 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1222)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1223)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1294 : nb078AlphaDummy1223 ∈ (SemanticCore.Class.cv nb078AlphaDummy1223).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1223).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1295 (h : SemanticCore.Var) : nb078AlphaDummy1226 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1226 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1226 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1296 : nb078AlphaDummy1050 ∈ (SemanticCore.Class.cv nb078AlphaDummy1051).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1050).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1297 : nb078AlphaDummy1050 ∈ (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_support_mem_1298 (h : SemanticCore.Var) : nb078AlphaDummy1053 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1054 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1053 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1299 (h : SemanticCore.Var) : nb078AlphaDummy1053 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_support_mem_1300 : nb078AlphaDummy1050 ∈ (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 ∪ (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

Certificates from NAR4C078C001Part031.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1301 (h : SemanticCore.Var) : nb078AlphaDummy1053 h ∈ (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 ∪ (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_support_mem_1302 : nb078AlphaDummy1208 ∈ (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_support_mem_1303 (h : SemanticCore.Var) : nb078AlphaDummy1210 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_support_mem_1304 : nb078AlphaDummy1208 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1208)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1208)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1305 (h : SemanticCore.Var) : nb078AlphaDummy1210 h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1210 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1210 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_compact_fv_empty_0026 : nb078AlphaDummy007 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_compact_fv_empty_0027 (f : SemanticCore.Var) : nb078AlphaDummy008 f ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_compact_fv_empty_0028 : nb078AlphaDummy005 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_compact_fv_empty_0029 (f : SemanticCore.Var) : nb078AlphaDummy006 f ∉ ∅

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_compact_fv_empty_0031 (f : SemanticCore.Var) : f ∉ ∅

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_compact_fv_empty_0033 (y : SemanticCore.Var) : y ∉ ∅

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_compact_fv_empty_0035 (x : SemanticCore.Var) : x ∉ ∅