NF weak partition development: NAR4H5C091M3BPart002.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_225 (D R : SemanticCore.Class) : nb091AlphaDummy060 D R ∉ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_distinct_226 (D R : SemanticCore.Class) : nb091AlphaDummy059 D R ≠ nb091AlphaDummy060 D R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_227 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy061 D R p ∉ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_228 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy062 D R p ∉ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_distinct_229 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy061 D R p ≠ nb091AlphaDummy062 D R p

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_230 (D R : SemanticCore.Class) : nb091AlphaDummy047 D R ∉ (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_231 (D R : SemanticCore.Class) : nb091AlphaDummy048 D R ∉ (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_distinct_232 (D R : SemanticCore.Class) : nb091AlphaDummy047 D R ≠ nb091AlphaDummy048 D R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_233 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy049 D R p ∉ (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_234 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy050 D R p ∉ (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_distinct_235 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy049 D R p ≠ nb091AlphaDummy050 D R p

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_236 (D R : SemanticCore.Class) : nb091AlphaDummy025 D R ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy020 D R)) (SemanticCore.Class.cv (nb091AlphaDummy021 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy020 D R)) (SemanticCore.Class.cv (nb091AlphaDummy021 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_237 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy026 D R p ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy023 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy024 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy023 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy024 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_238 (D R : SemanticCore.Class) : nb091AlphaDummy085 D R ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy080 D R)) (SemanticCore.Class.cv (nb091AlphaDummy081 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy080 D R)) (SemanticCore.Class.cv (nb091AlphaDummy081 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_239 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy086 D R p ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy083 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy084 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy083 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy084 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_240 (D R : SemanticCore.Class) : nb091AlphaDummy139 D R ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy134 D R)) (SemanticCore.Class.cv (nb091AlphaDummy135 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy134 D R)) (SemanticCore.Class.cv (nb091AlphaDummy135 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_241 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy140 R p ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy137 R p)) (SemanticCore.Class.cv (nb091AlphaDummy138 R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy137 R p)) (SemanticCore.Class.cv (nb091AlphaDummy138 R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_242 (D R : SemanticCore.Class) : nb091AlphaDummy167 D R ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy162 D R)) (SemanticCore.Class.cv (nb091AlphaDummy163 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy162 D R)) (SemanticCore.Class.cv (nb091AlphaDummy163 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_243 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy168 D R p ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy165 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy166 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy165 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy166 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_244 (D R : SemanticCore.Class) : nb091AlphaDummy203 D R ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy198 D R)) (SemanticCore.Class.cv (nb091AlphaDummy199 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy198 D R)) (SemanticCore.Class.cv (nb091AlphaDummy199 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_245 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy204 D R p ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy201 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy202 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy201 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy202 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_246 (D R : SemanticCore.Class) : nb091AlphaDummy101 D R ∉ (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_247 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy102 D R p ∉ (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_248 (D R : SemanticCore.Class) : nb091AlphaDummy055 D R ∉ (Compiler.CompactSourceSyntax.synCnin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_249 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy056 D R p ∉ (Compiler.CompactSourceSyntax.synCnin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_250 (D R : SemanticCore.Class) : nb091AlphaDummy039 D R ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_251 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy040 D R p ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_252 (D R : SemanticCore.Class) : nb091AlphaDummy181 D R ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy048 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy048 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_253 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy182 D R p ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy050 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy050 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_254 (D R : SemanticCore.Class) : nb091AlphaDummy099 D R ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_255 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy100 D R p ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_256 (D R : SemanticCore.Class) : nb091AlphaDummy153 D R ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_257 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy154 R p ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_258 (D R : SemanticCore.Class) : nb091AlphaDummy217 D R ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_259 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy218 D R p ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_260 (D R : SemanticCore.Class) : nb091AlphaDummy111 D R ∉ (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_261 (D R : SemanticCore.Class) : nb091AlphaDummy112 D R ∉ (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_distinct_262 (D R : SemanticCore.Class) : nb091AlphaDummy111 D R ≠ nb091AlphaDummy112 D R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_263 (p : SemanticCore.Var) : nb091AlphaDummy113 p ∉ (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_264 (p : SemanticCore.Var) : nb091AlphaDummy114 p ∉ (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_distinct_265 (p : SemanticCore.Var) : nb091AlphaDummy113 p ≠ nb091AlphaDummy114 p

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_266 (D R : SemanticCore.Class) : nb091AlphaDummy109 D R ∉ (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_267 (p : SemanticCore.Var) : nb091AlphaDummy110 p ∉ (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_268 (D R : SemanticCore.Class) : nb091AlphaDummy103 D R ∉ D.fv ∪ (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_269 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy104 D R p ∉ D.fv ∪ (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_270 (D R : SemanticCore.Class) : nb091AlphaDummy057 D R ∉ R.fv ∪ (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_271 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy058 D R p ∉ R.fv ∪ (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_272 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∉ R.fv ∪ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_273 (D R : SemanticCore.Class) : nb091AlphaDummy001 D R ∉ {nb091AlphaDummy000 D R} ∪ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv ∪ (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))) (Compiler.CompactSourceSyntax.synChwniso D)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_274 (D R : SemanticCore.Class) : nb091AlphaDummy003 D R ∉ {nb091AlphaDummy000 D R} ∪ {nb091AlphaDummy001 D R} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy000 D R)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy001 D R)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))) (Compiler.CompactSourceSyntax.synChwniso D)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_275 (D R : SemanticCore.Class) : nb091AlphaDummy063 D R ∉ {nb091AlphaDummy059 D R} ∪ {nb091AlphaDummy060 D R} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy059 D R)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy060 D R)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_276 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy064 D R p ∉ {nb091AlphaDummy061 D R p} ∪ {nb091AlphaDummy062 D R p} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy061 D R p)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy062 D R p)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_277 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy002 D R p ∉ {p} ∪ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv ∪ (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))) (Compiler.CompactSourceSyntax.synChwniso D)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_fresh_278 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy004 D R p ∉ {p} ∪ {nb091AlphaDummy002 D R p} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy002 D R p)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))) (Compiler.CompactSourceSyntax.synChwniso D)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0000 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ {nb091AlphaDummy000 D R} ∪ {nb091AlphaDummy001 D R} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy000 D R)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy001 D R)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))) (Compiler.CompactSourceSyntax.synChwniso D)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0001 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ {p} ∪ {nb091AlphaDummy002 D R p} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy002 D R p)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))) (Compiler.CompactSourceSyntax.synChwniso D)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0002 (D R : SemanticCore.Class) : nb091AlphaDummy001 D R ∈ {nb091AlphaDummy000 D R} ∪ {nb091AlphaDummy001 D R} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy000 D R)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy001 D R)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))) (Compiler.CompactSourceSyntax.synChwniso D)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0003 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy002 D R p ∈ {p} ∪ {nb091AlphaDummy002 D R p} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy002 D R p)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))) (Compiler.CompactSourceSyntax.synChwniso D)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0004 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ {nb091AlphaDummy000 D R} ∪ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv ∪ (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))) (Compiler.CompactSourceSyntax.synChwniso D)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0005 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ {p} ∪ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv ∪ (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))) (Compiler.CompactSourceSyntax.synChwniso D)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0006 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy000 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy001 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0007 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy005 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy006 D R) (SemanticCore.Class.cv (nb091AlphaDummy000 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy005 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy005 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy006 D R) (SemanticCore.Class.cv (nb091AlphaDummy001 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy005 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0008 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (SemanticCore.Class.cv p).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy002 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0009 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy007 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy008 D R p) (SemanticCore.Class.cv p) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy007 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy007 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy008 D R p) (SemanticCore.Class.cv (nb091AlphaDummy002 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy007 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0010 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (SemanticCore.Class.cab (nb091AlphaDummy005 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy006 D R) (SemanticCore.Class.cv (nb091AlphaDummy000 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy005 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R)))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy005 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy006 D R) (SemanticCore.Class.cv (nb091AlphaDummy000 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy005 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0011 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (SemanticCore.Class.cab (nb091AlphaDummy007 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy008 D R p) (SemanticCore.Class.cv p) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy007 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p)))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy007 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy008 D R p) (SemanticCore.Class.cv p) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy007 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0012 (D R : SemanticCore.Class) : nb091AlphaDummy006 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy006 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0013 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy008 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy008 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0014 (D R : SemanticCore.Class) : nb091AlphaDummy013 D R ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy013 D R)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb091AlphaDummy013 D R)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy013 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0015 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy015 D R p ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy015 D R p)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb091AlphaDummy015 D R p)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy015 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0016 (D R : SemanticCore.Class) : nb091AlphaDummy013 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy013 D R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0017 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy015 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy015 D R p)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0018 (D R : SemanticCore.Class) : nb091AlphaDummy020 D R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy020 D R)) (SemanticCore.Class.cv (nb091AlphaDummy021 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy020 D R)) (SemanticCore.Class.cv (nb091AlphaDummy021 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0019 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy023 D R p ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy023 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy024 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy023 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy024 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0020 (D R : SemanticCore.Class) : nb091AlphaDummy020 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy020 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy021 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0021 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy023 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy023 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy024 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0022 (D R : SemanticCore.Class) : nb091AlphaDummy021 D R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy020 D R)) (SemanticCore.Class.cv (nb091AlphaDummy021 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy020 D R)) (SemanticCore.Class.cv (nb091AlphaDummy021 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0023 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy024 D R p ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy023 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy024 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy023 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy024 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0024 (D R : SemanticCore.Class) : nb091AlphaDummy021 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy020 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy021 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0025 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy024 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy023 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy024 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0026 (D R : SemanticCore.Class) : nb091AlphaDummy020 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy020 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy021 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0027 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy023 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy023 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy024 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0028 (D R : SemanticCore.Class) : nb091AlphaDummy020 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy020 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy020 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0029 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy023 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy023 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy023 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0030 (D R : SemanticCore.Class) : nb091AlphaDummy021 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy020 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy021 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0031 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy024 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy023 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy024 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0032 (D R : SemanticCore.Class) : nb091AlphaDummy021 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy021 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy021 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0033 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy024 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy024 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy024 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0034 (D R : SemanticCore.Class) : nb091AlphaDummy001 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy000 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy001 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0035 (D R : SemanticCore.Class) : nb091AlphaDummy001 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy005 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy006 D R) (SemanticCore.Class.cv (nb091AlphaDummy000 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy005 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy005 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy006 D R) (SemanticCore.Class.cv (nb091AlphaDummy001 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy005 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0036 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy002 D R p ∈ (SemanticCore.Class.cv p).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy002 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0037 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy002 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy007 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy008 D R p) (SemanticCore.Class.cv p) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy007 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy007 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy008 D R p) (SemanticCore.Class.cv (nb091AlphaDummy002 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy007 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0038 (D R : SemanticCore.Class) : nb091AlphaDummy001 D R ∈ (SemanticCore.Class.cab (nb091AlphaDummy005 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy006 D R) (SemanticCore.Class.cv (nb091AlphaDummy001 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy005 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy005 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy006 D R) (SemanticCore.Class.cv (nb091AlphaDummy001 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy005 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0039 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy002 D R p ∈ (SemanticCore.Class.cab (nb091AlphaDummy007 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy008 D R p) (SemanticCore.Class.cv (nb091AlphaDummy002 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy007 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy007 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy008 D R p) (SemanticCore.Class.cv (nb091AlphaDummy002 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy007 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0040 (D R : SemanticCore.Class) : nb091AlphaDummy006 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0041 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy008 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0042 (D R : SemanticCore.Class) : nb091AlphaDummy006 D R ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0043 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy008 D R p ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0044 (D R : SemanticCore.Class) : nb091AlphaDummy059 D R ∈ {nb091AlphaDummy059 D R} ∪ {nb091AlphaDummy060 D R} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy059 D R)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy060 D R)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0045 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy061 D R p ∈ {nb091AlphaDummy061 D R p} ∪ {nb091AlphaDummy062 D R p} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy061 D R p)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy062 D R p)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0046 (D R : SemanticCore.Class) : nb091AlphaDummy060 D R ∈ {nb091AlphaDummy059 D R} ∪ {nb091AlphaDummy060 D R} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy059 D R)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy060 D R)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0047 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy062 D R p ∈ {nb091AlphaDummy061 D R p} ∪ {nb091AlphaDummy062 D R p} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy061 D R p)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy062 D R p)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0048 (D R : SemanticCore.Class) : nb091AlphaDummy059 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy059 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy060 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0049 (D R : SemanticCore.Class) : nb091AlphaDummy059 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy065 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy066 D R) (SemanticCore.Class.cv (nb091AlphaDummy059 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy065 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy065 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy066 D R) (SemanticCore.Class.cv (nb091AlphaDummy060 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy065 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0050 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy061 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy061 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy062 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0051 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy061 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy067 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy068 D R p) (SemanticCore.Class.cv (nb091AlphaDummy061 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy067 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy067 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy068 D R p) (SemanticCore.Class.cv (nb091AlphaDummy062 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy067 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0052 (D R : SemanticCore.Class) : nb091AlphaDummy059 D R ∈ (SemanticCore.Class.cab (nb091AlphaDummy065 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy066 D R) (SemanticCore.Class.cv (nb091AlphaDummy059 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy065 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R)))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy065 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy066 D R) (SemanticCore.Class.cv (nb091AlphaDummy059 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy065 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0053 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy061 D R p ∈ (SemanticCore.Class.cab (nb091AlphaDummy067 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy068 D R p) (SemanticCore.Class.cv (nb091AlphaDummy061 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy067 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p)))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy067 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy068 D R p) (SemanticCore.Class.cv (nb091AlphaDummy061 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy067 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0054 (D R : SemanticCore.Class) : nb091AlphaDummy066 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy066 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0055 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy068 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy068 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0056 (D R : SemanticCore.Class) : nb091AlphaDummy073 D R ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy073 D R)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb091AlphaDummy073 D R)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy073 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0057 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy075 D R p ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy075 D R p)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb091AlphaDummy075 D R p)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy075 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0058 (D R : SemanticCore.Class) : nb091AlphaDummy073 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy073 D R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0059 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy075 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy075 D R p)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0060 (D R : SemanticCore.Class) : nb091AlphaDummy080 D R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy080 D R)) (SemanticCore.Class.cv (nb091AlphaDummy081 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy080 D R)) (SemanticCore.Class.cv (nb091AlphaDummy081 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0061 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy083 D R p ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy083 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy084 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy083 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy084 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0062 (D R : SemanticCore.Class) : nb091AlphaDummy080 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy080 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy081 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0063 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy083 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy083 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy084 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0064 (D R : SemanticCore.Class) : nb091AlphaDummy081 D R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy080 D R)) (SemanticCore.Class.cv (nb091AlphaDummy081 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy080 D R)) (SemanticCore.Class.cv (nb091AlphaDummy081 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0065 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy084 D R p ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy083 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy084 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy083 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy084 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0066 (D R : SemanticCore.Class) : nb091AlphaDummy081 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy080 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy081 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0067 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy084 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy083 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy084 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0068 (D R : SemanticCore.Class) : nb091AlphaDummy080 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy080 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy081 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0069 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy083 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy083 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy084 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0070 (D R : SemanticCore.Class) : nb091AlphaDummy080 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy080 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy080 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0071 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy083 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy083 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy083 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0072 (D R : SemanticCore.Class) : nb091AlphaDummy081 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy080 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy081 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0073 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy084 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy083 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy084 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0074 (D R : SemanticCore.Class) : nb091AlphaDummy081 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy081 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy081 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0075 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy084 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy084 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy084 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0076 (D R : SemanticCore.Class) : nb091AlphaDummy060 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy059 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy060 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0077 (D R : SemanticCore.Class) : nb091AlphaDummy060 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy065 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy066 D R) (SemanticCore.Class.cv (nb091AlphaDummy059 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy065 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy065 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy066 D R) (SemanticCore.Class.cv (nb091AlphaDummy060 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy065 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0078 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy062 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy061 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy062 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0079 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy062 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy067 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy068 D R p) (SemanticCore.Class.cv (nb091AlphaDummy061 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy067 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy067 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy068 D R p) (SemanticCore.Class.cv (nb091AlphaDummy062 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy067 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0080 (D R : SemanticCore.Class) : nb091AlphaDummy060 D R ∈ (SemanticCore.Class.cab (nb091AlphaDummy065 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy066 D R) (SemanticCore.Class.cv (nb091AlphaDummy060 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy065 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy065 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy066 D R) (SemanticCore.Class.cv (nb091AlphaDummy060 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy065 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0081 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy062 D R p ∈ (SemanticCore.Class.cab (nb091AlphaDummy067 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy068 D R p) (SemanticCore.Class.cv (nb091AlphaDummy062 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy067 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy067 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy068 D R p) (SemanticCore.Class.cv (nb091AlphaDummy062 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy067 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0082 (D R : SemanticCore.Class) : nb091AlphaDummy066 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0083 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy068 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0084 (D R : SemanticCore.Class) : nb091AlphaDummy066 D R ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy066 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0085 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy068 D R p ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy068 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0086 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (Compiler.CompactSourceSyntax.synChwniso D).fv ∪ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0087 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (Compiler.CompactSourceSyntax.synChwniso D).fv ∪ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0088 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0089 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0090 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0091 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy047 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy048 D R) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy047 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy048 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy047 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy048 D R) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy047 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy048 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0092 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0093 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy049 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy050 D R p) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy049 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy050 D R p))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy049 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy050 D R p) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy049 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy050 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0094 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (SemanticCore.Class.cab (nb091AlphaDummy047 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy048 D R) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy047 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy048 D R)))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy047 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy048 D R) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy047 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy048 D R)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0095 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (SemanticCore.Class.cab (nb091AlphaDummy049 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy050 D R p) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy049 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy050 D R p)))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy049 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy050 D R p) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy049 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy050 D R p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0096 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (Compiler.CompactSourceSyntax.synCnin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0097 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (Compiler.CompactSourceSyntax.synCnin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0098 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ R.fv ∪ (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0099 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ R.fv ∪ (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0100 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ {nb091AlphaDummy059 D R} ∪ {nb091AlphaDummy060 D R} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy059 D R)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy060 D R)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0101 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ {nb091AlphaDummy061 D R p} ∪ {nb091AlphaDummy062 D R p} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy061 D R p)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy062 D R p)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0102 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0103 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0104 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0105 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0106 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ D.fv ∪ (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0107 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ D.fv ∪ (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0108 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv ∪ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0109 (R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv ∪ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0110 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0111 (p : SemanticCore.Var) : p ∈ (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0112 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0113 (p : SemanticCore.Var) : p ∈ (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0114 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy000 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0115 (p : SemanticCore.Var) : p ∈ (SemanticCore.Class.cv p).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0116 (D R : SemanticCore.Class) : nb091AlphaDummy106 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy106 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy105 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0117 (D R : SemanticCore.Class) : nb091AlphaDummy106 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy119 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy120 D R) (SemanticCore.Class.cv (nb091AlphaDummy106 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy119 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy119 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy120 D R) (SemanticCore.Class.cv (nb091AlphaDummy105 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy119 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0118 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy108 R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy108 R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy107 R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0119 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy108 R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy121 R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy122 R p) (SemanticCore.Class.cv (nb091AlphaDummy108 R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy121 R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy121 R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy122 R p) (SemanticCore.Class.cv (nb091AlphaDummy107 R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy121 R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0120 (D R : SemanticCore.Class) : nb091AlphaDummy106 D R ∈ (SemanticCore.Class.cab (nb091AlphaDummy119 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy120 D R) (SemanticCore.Class.cv (nb091AlphaDummy106 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy119 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R)))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy119 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy120 D R) (SemanticCore.Class.cv (nb091AlphaDummy106 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy119 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0121 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy108 R p ∈ (SemanticCore.Class.cab (nb091AlphaDummy121 R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy122 R p) (SemanticCore.Class.cv (nb091AlphaDummy108 R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy121 R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p)))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy121 R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy122 R p) (SemanticCore.Class.cv (nb091AlphaDummy108 R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy121 R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0122 (D R : SemanticCore.Class) : nb091AlphaDummy120 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy120 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0123 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy122 R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy122 R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0124 (D R : SemanticCore.Class) : nb091AlphaDummy127 D R ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy127 D R)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb091AlphaDummy127 D R)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy127 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0125 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy129 R p ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy129 R p)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb091AlphaDummy129 R p)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy129 R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0126 (D R : SemanticCore.Class) : nb091AlphaDummy127 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy127 D R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0127 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy129 R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy129 R p)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0128 (D R : SemanticCore.Class) : nb091AlphaDummy134 D R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy134 D R)) (SemanticCore.Class.cv (nb091AlphaDummy135 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy134 D R)) (SemanticCore.Class.cv (nb091AlphaDummy135 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0129 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy137 R p ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy137 R p)) (SemanticCore.Class.cv (nb091AlphaDummy138 R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy137 R p)) (SemanticCore.Class.cv (nb091AlphaDummy138 R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0130 (D R : SemanticCore.Class) : nb091AlphaDummy134 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy134 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy135 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0131 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy137 R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy137 R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy138 R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0132 (D R : SemanticCore.Class) : nb091AlphaDummy135 D R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy134 D R)) (SemanticCore.Class.cv (nb091AlphaDummy135 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy134 D R)) (SemanticCore.Class.cv (nb091AlphaDummy135 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0133 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy138 R p ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy137 R p)) (SemanticCore.Class.cv (nb091AlphaDummy138 R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy137 R p)) (SemanticCore.Class.cv (nb091AlphaDummy138 R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0134 (D R : SemanticCore.Class) : nb091AlphaDummy135 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy134 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy135 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0135 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy138 R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy137 R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy138 R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0136 (D R : SemanticCore.Class) : nb091AlphaDummy134 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy134 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy135 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0137 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy137 R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy137 R p))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy138 R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0138 (D R : SemanticCore.Class) : nb091AlphaDummy134 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy134 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy134 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0139 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy137 R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy137 R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy137 R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0140 (D R : SemanticCore.Class) : nb091AlphaDummy135 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy134 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy135 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0141 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy138 R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy137 R p))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy138 R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0142 (D R : SemanticCore.Class) : nb091AlphaDummy135 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy135 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy135 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0143 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy138 R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy138 R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy138 R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0144 (D R : SemanticCore.Class) : nb091AlphaDummy105 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy106 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy105 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0145 (D R : SemanticCore.Class) : nb091AlphaDummy105 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy119 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy120 D R) (SemanticCore.Class.cv (nb091AlphaDummy106 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy119 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy119 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy120 D R) (SemanticCore.Class.cv (nb091AlphaDummy105 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy119 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0146 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy107 R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy108 R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy107 R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0147 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy107 R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy121 R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy122 R p) (SemanticCore.Class.cv (nb091AlphaDummy108 R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy121 R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy121 R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy122 R p) (SemanticCore.Class.cv (nb091AlphaDummy107 R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy121 R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0148 (D R : SemanticCore.Class) : nb091AlphaDummy105 D R ∈ (SemanticCore.Class.cab (nb091AlphaDummy119 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy120 D R) (SemanticCore.Class.cv (nb091AlphaDummy105 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy119 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy119 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy120 D R) (SemanticCore.Class.cv (nb091AlphaDummy105 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy119 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0149 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy107 R p ∈ (SemanticCore.Class.cab (nb091AlphaDummy121 R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy122 R p) (SemanticCore.Class.cv (nb091AlphaDummy107 R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy121 R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy121 R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy122 R p) (SemanticCore.Class.cv (nb091AlphaDummy107 R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy121 R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0150 (D R : SemanticCore.Class) : nb091AlphaDummy120 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0151 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy122 R p ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0152 (D R : SemanticCore.Class) : nb091AlphaDummy120 D R ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy120 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0153 (R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy122 R p ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy122 R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0154 (D R : SemanticCore.Class) : nb091AlphaDummy048 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy048 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0155 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy050 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy050 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0156 (D R : SemanticCore.Class) : nb091AlphaDummy155 D R ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy155 D R)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb091AlphaDummy155 D R)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy155 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0157 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy157 D R p ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy157 D R p)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb091AlphaDummy157 D R p)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy157 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0158 (D R : SemanticCore.Class) : nb091AlphaDummy155 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy155 D R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0159 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy157 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy157 D R p)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0160 (D R : SemanticCore.Class) : nb091AlphaDummy162 D R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy162 D R)) (SemanticCore.Class.cv (nb091AlphaDummy163 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy162 D R)) (SemanticCore.Class.cv (nb091AlphaDummy163 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0161 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy165 D R p ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy165 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy166 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy165 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy166 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0162 (D R : SemanticCore.Class) : nb091AlphaDummy162 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy162 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy163 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0163 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy165 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy165 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy166 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0164 (D R : SemanticCore.Class) : nb091AlphaDummy163 D R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy162 D R)) (SemanticCore.Class.cv (nb091AlphaDummy163 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy162 D R)) (SemanticCore.Class.cv (nb091AlphaDummy163 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0165 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy166 D R p ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy165 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy166 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy165 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy166 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0166 (D R : SemanticCore.Class) : nb091AlphaDummy163 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy162 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy163 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0167 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy166 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy165 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy166 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0168 (D R : SemanticCore.Class) : nb091AlphaDummy162 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy162 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy163 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0169 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy165 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy165 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy166 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0170 (D R : SemanticCore.Class) : nb091AlphaDummy162 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy162 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy162 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0171 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy165 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy165 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy165 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0172 (D R : SemanticCore.Class) : nb091AlphaDummy163 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy162 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy163 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0173 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy166 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy165 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy166 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0174 (D R : SemanticCore.Class) : nb091AlphaDummy163 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy163 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy163 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0175 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy166 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy166 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy166 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0176 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∈ (SemanticCore.Class.cab (nb091AlphaDummy047 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy048 D R) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy047 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy048 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy047 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy048 D R) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv (nb091AlphaDummy000 D R))))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy047 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy048 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0177 (D R : SemanticCore.Class) (p : SemanticCore.Var) : p ∈ (SemanticCore.Class.cab (nb091AlphaDummy049 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy050 D R p) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy049 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy050 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy049 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy050 D R p) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy049 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy050 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0178 (D R : SemanticCore.Class) : nb091AlphaDummy048 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy048 D R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0179 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy050 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy050 D R p)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0180 (D R : SemanticCore.Class) : nb091AlphaDummy048 D R ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy048 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy048 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0181 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy050 D R p ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy050 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy050 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0182 (D R : SemanticCore.Class) : nb091AlphaDummy042 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy042 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy041 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0183 (D R : SemanticCore.Class) : nb091AlphaDummy042 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy183 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy184 D R) (SemanticCore.Class.cv (nb091AlphaDummy042 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy183 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy183 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy184 D R) (SemanticCore.Class.cv (nb091AlphaDummy041 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy183 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0184 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy044 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy044 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy043 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0185 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy044 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy185 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy186 D R p) (SemanticCore.Class.cv (nb091AlphaDummy044 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy185 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy185 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy186 D R p) (SemanticCore.Class.cv (nb091AlphaDummy043 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy185 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0186 (D R : SemanticCore.Class) : nb091AlphaDummy042 D R ∈ (SemanticCore.Class.cab (nb091AlphaDummy183 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy184 D R) (SemanticCore.Class.cv (nb091AlphaDummy042 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy183 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R)))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy183 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy184 D R) (SemanticCore.Class.cv (nb091AlphaDummy042 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy183 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0187 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy044 D R p ∈ (SemanticCore.Class.cab (nb091AlphaDummy185 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy186 D R p) (SemanticCore.Class.cv (nb091AlphaDummy044 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy185 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p)))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy185 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy186 D R p) (SemanticCore.Class.cv (nb091AlphaDummy044 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy185 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0188 (D R : SemanticCore.Class) : nb091AlphaDummy184 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy184 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0189 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy186 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy186 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0190 (D R : SemanticCore.Class) : nb091AlphaDummy191 D R ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy191 D R)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb091AlphaDummy191 D R)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy191 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0191 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy193 D R p ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy193 D R p)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb091AlphaDummy193 D R p)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy193 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0192 (D R : SemanticCore.Class) : nb091AlphaDummy191 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy191 D R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0193 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy193 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy193 D R p)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0194 (D R : SemanticCore.Class) : nb091AlphaDummy198 D R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy198 D R)) (SemanticCore.Class.cv (nb091AlphaDummy199 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy198 D R)) (SemanticCore.Class.cv (nb091AlphaDummy199 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0195 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy201 D R p ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy201 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy202 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy201 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy202 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0196 (D R : SemanticCore.Class) : nb091AlphaDummy198 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy198 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy199 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0197 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy201 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy201 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy202 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0198 (D R : SemanticCore.Class) : nb091AlphaDummy199 D R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy198 D R)) (SemanticCore.Class.cv (nb091AlphaDummy199 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy198 D R)) (SemanticCore.Class.cv (nb091AlphaDummy199 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0199 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy202 D R p ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy201 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy202 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb091AlphaDummy201 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy202 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0200 (D R : SemanticCore.Class) : nb091AlphaDummy199 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy198 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy199 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0201 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy202 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy201 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy202 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0202 (D R : SemanticCore.Class) : nb091AlphaDummy198 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy198 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy199 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0203 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy201 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy201 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy202 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0204 (D R : SemanticCore.Class) : nb091AlphaDummy198 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy198 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy198 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0205 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy201 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy201 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy201 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0206 (D R : SemanticCore.Class) : nb091AlphaDummy199 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy198 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy199 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0207 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy202 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy201 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb091AlphaDummy202 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0208 (D R : SemanticCore.Class) : nb091AlphaDummy199 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy199 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy199 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0209 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy202 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy202 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy202 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0210 (D R : SemanticCore.Class) : nb091AlphaDummy041 D R ∈ (SemanticCore.Class.cv (nb091AlphaDummy042 D R)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy041 D R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0211 (D R : SemanticCore.Class) : nb091AlphaDummy041 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy183 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy184 D R) (SemanticCore.Class.cv (nb091AlphaDummy042 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy183 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy183 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy184 D R) (SemanticCore.Class.cv (nb091AlphaDummy041 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy183 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0212 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy043 D R p ∈ (SemanticCore.Class.cv (nb091AlphaDummy044 D R p)).fv ∪ (SemanticCore.Class.cv (nb091AlphaDummy043 D R p)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0213 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy043 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy185 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy186 D R p) (SemanticCore.Class.cv (nb091AlphaDummy044 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy185 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy185 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy186 D R p) (SemanticCore.Class.cv (nb091AlphaDummy043 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy185 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0214 (D R : SemanticCore.Class) : nb091AlphaDummy041 D R ∈ (SemanticCore.Class.cab (nb091AlphaDummy183 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy184 D R) (SemanticCore.Class.cv (nb091AlphaDummy041 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy183 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy183 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy184 D R) (SemanticCore.Class.cv (nb091AlphaDummy041 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy183 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0215 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy043 D R p ∈ (SemanticCore.Class.cab (nb091AlphaDummy185 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy186 D R p) (SemanticCore.Class.cv (nb091AlphaDummy043 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy185 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb091AlphaDummy185 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy186 D R p) (SemanticCore.Class.cv (nb091AlphaDummy043 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy185 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0216 (D R : SemanticCore.Class) : nb091AlphaDummy184 D R ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0217 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy186 D R p ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0218 (D R : SemanticCore.Class) : nb091AlphaDummy184 D R ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_support_mem_0219 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy186 D R p ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0020 (D R : SemanticCore.Class) : nb091AlphaDummy001 D R ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0021 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy002 D R p ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0022 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0023 (p : SemanticCore.Var) : p ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0024 (D R : SemanticCore.Class) : nb091AlphaDummy003 D R ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0025 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy004 D R p ∉ ∅