Nominal proof certificates grouped in dependency order.

Certificates from NAR4C068C001Part010.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0076 (f : SemanticCore.Var) : nb068AlphaDummy049 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy048 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy049 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0077 (f : SemanticCore.Var) : nb068AlphaDummy049 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy056 f) (SemanticCore.Class.cv (nb068AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy056 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0078 : nb068AlphaDummy046 ∈ (SemanticCore.Class.cab nb068AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy054 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy054 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0079 (f : SemanticCore.Var) : nb068AlphaDummy049 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy056 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy056 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0080 : nb068AlphaDummy054 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0081 (f : SemanticCore.Var) : nb068AlphaDummy056 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0082 : nb068AlphaDummy054 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0083 (f : SemanticCore.Var) : nb068AlphaDummy056 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0084 : nb068AlphaDummy045 ∈ (SemanticCore.Class.cv nb068AlphaDummy045).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy047).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0085 : nb068AlphaDummy045 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0086 (f : SemanticCore.Var) : nb068AlphaDummy048 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy048 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy050 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0087 (f : SemanticCore.Var) : nb068AlphaDummy048 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0088 : nb068AlphaDummy045 ∈ (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0089 (f : SemanticCore.Var) : nb068AlphaDummy048 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f)))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0090 : nb068AlphaDummy090 ∈ (SemanticCore.Class.cv nb068AlphaDummy090).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0091 (f : SemanticCore.Var) : nb068AlphaDummy092 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy092 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0093 (f : SemanticCore.Var) : nb068AlphaDummy099 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy099 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy099 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy099 f)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0096 : nb068AlphaDummy104 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0097 (f : SemanticCore.Var) : nb068AlphaDummy107 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0098 : nb068AlphaDummy104 ∈ (SemanticCore.Class.cv nb068AlphaDummy104).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy105).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0099 (f : SemanticCore.Var) : nb068AlphaDummy107 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy107 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy108 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0100 : nb068AlphaDummy105 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0101 (f : SemanticCore.Var) : nb068AlphaDummy108 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0102 : nb068AlphaDummy105 ∈ (SemanticCore.Class.cv nb068AlphaDummy104).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy105).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0103 (f : SemanticCore.Var) : nb068AlphaDummy108 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy107 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy108 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0104 : nb068AlphaDummy104 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy104)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy105)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0105 (f : SemanticCore.Var) : nb068AlphaDummy107 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy107 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy108 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0106 : nb068AlphaDummy104 ∈ (SemanticCore.Class.cv nb068AlphaDummy104).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy104).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0108 : nb068AlphaDummy105 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy104)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy105)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0109 (f : SemanticCore.Var) : nb068AlphaDummy108 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy107 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy108 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0110 : nb068AlphaDummy105 ∈ (SemanticCore.Class.cv nb068AlphaDummy105).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy105).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0112 : nb068AlphaDummy047 ∈ (SemanticCore.Class.cv nb068AlphaDummy045).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy047).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0113 : nb068AlphaDummy047 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0114 (f : SemanticCore.Var) : nb068AlphaDummy050 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy048 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy050 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0115 (f : SemanticCore.Var) : nb068AlphaDummy050 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0116 : nb068AlphaDummy047 ∈ (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0117 (f : SemanticCore.Var) : nb068AlphaDummy050 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0118 : nb068AlphaDummy090 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0119 (f : SemanticCore.Var) : nb068AlphaDummy092 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0120 : nb068AlphaDummy090 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0121 (f : SemanticCore.Var) : nb068AlphaDummy092 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0122 : nb068AlphaDummy125 ∈ {nb068AlphaDummy125} ∪ {nb068AlphaDummy126} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Class.cv nb068AlphaDummy000) (SemanticCore.Class.cv nb068AlphaDummy125)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0123 (f : SemanticCore.Var) : nb068AlphaDummy127 f ∈ {nb068AlphaDummy127 f} ∪ {nb068AlphaDummy128 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb068AlphaDummy127 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0124 : nb068AlphaDummy126 ∈ {nb068AlphaDummy125} ∪ {nb068AlphaDummy126} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Class.cv nb068AlphaDummy000) (SemanticCore.Class.cv nb068AlphaDummy125)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0125 (f : SemanticCore.Var) : nb068AlphaDummy128 f ∈ {nb068AlphaDummy127 f} ∪ {nb068AlphaDummy128 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb068AlphaDummy127 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0126 : nb068AlphaDummy125 ∈ (SemanticCore.Class.cv nb068AlphaDummy125).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy126).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0127 : nb068AlphaDummy125 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0128 (f : SemanticCore.Var) : nb068AlphaDummy127 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy127 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy128 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0129 (f : SemanticCore.Var) : nb068AlphaDummy127 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0130 : nb068AlphaDummy125 ∈ (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0131 (f : SemanticCore.Var) : nb068AlphaDummy127 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f)))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0132 : nb068AlphaDummy132 ∈ (SemanticCore.Class.cv nb068AlphaDummy132).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0133 (f : SemanticCore.Var) : nb068AlphaDummy134 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy134 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0135 (f : SemanticCore.Var) : nb068AlphaDummy141 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy141 f)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0138 : nb068AlphaDummy146 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0139 (f : SemanticCore.Var) : nb068AlphaDummy149 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0140 : nb068AlphaDummy146 ∈ (SemanticCore.Class.cv nb068AlphaDummy146).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy147).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0141 (f : SemanticCore.Var) : nb068AlphaDummy149 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy149 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy150 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0142 : nb068AlphaDummy147 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0143 (f : SemanticCore.Var) : nb068AlphaDummy150 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0144 : nb068AlphaDummy147 ∈ (SemanticCore.Class.cv nb068AlphaDummy146).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy147).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0145 (f : SemanticCore.Var) : nb068AlphaDummy150 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy149 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy150 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0146 : nb068AlphaDummy146 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy146)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy147)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0147 (f : SemanticCore.Var) : nb068AlphaDummy149 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy149 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy150 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0148 : nb068AlphaDummy146 ∈ (SemanticCore.Class.cv nb068AlphaDummy146).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy146).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0150 : nb068AlphaDummy147 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy146)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy147)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0151 (f : SemanticCore.Var) : nb068AlphaDummy150 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy149 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy150 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0152 : nb068AlphaDummy147 ∈ (SemanticCore.Class.cv nb068AlphaDummy147).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy147).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0154 : nb068AlphaDummy126 ∈ (SemanticCore.Class.cv nb068AlphaDummy125).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy126).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0155 : nb068AlphaDummy126 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0156 (f : SemanticCore.Var) : nb068AlphaDummy128 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy127 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy128 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0157 (f : SemanticCore.Var) : nb068AlphaDummy128 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0158 : nb068AlphaDummy126 ∈ (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0159 (f : SemanticCore.Var) : nb068AlphaDummy128 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0160 : nb068AlphaDummy132 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0161 (f : SemanticCore.Var) : nb068AlphaDummy134 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0162 : nb068AlphaDummy132 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0163 (f : SemanticCore.Var) : nb068AlphaDummy134 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0164 : nb068AlphaDummy126 ∈ (SemanticCore.Class.cv nb068AlphaDummy126).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy125).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0165 : nb068AlphaDummy126 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0166 (f : SemanticCore.Var) : nb068AlphaDummy128 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy128 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy127 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0167 (f : SemanticCore.Var) : nb068AlphaDummy128 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0168 : nb068AlphaDummy126 ∈ (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0169 (f : SemanticCore.Var) : nb068AlphaDummy128 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f)))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0170 : nb068AlphaDummy168 ∈ (SemanticCore.Class.cv nb068AlphaDummy168).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0171 (f : SemanticCore.Var) : nb068AlphaDummy170 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy170 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0173 (f : SemanticCore.Var) : nb068AlphaDummy177 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy177 f)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0176 : nb068AlphaDummy182 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0177 (f : SemanticCore.Var) : nb068AlphaDummy185 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0178 : nb068AlphaDummy182 ∈ (SemanticCore.Class.cv nb068AlphaDummy182).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy183).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0179 (f : SemanticCore.Var) : nb068AlphaDummy185 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy185 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy186 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0180 : nb068AlphaDummy183 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0181 (f : SemanticCore.Var) : nb068AlphaDummy186 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0182 : nb068AlphaDummy183 ∈ (SemanticCore.Class.cv nb068AlphaDummy182).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy183).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0183 (f : SemanticCore.Var) : nb068AlphaDummy186 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy185 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy186 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0184 : nb068AlphaDummy182 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy182)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy183)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0185 (f : SemanticCore.Var) : nb068AlphaDummy185 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy185 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy186 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0186 : nb068AlphaDummy182 ∈ (SemanticCore.Class.cv nb068AlphaDummy182).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy182).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0188 : nb068AlphaDummy183 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy182)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy183)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0189 (f : SemanticCore.Var) : nb068AlphaDummy186 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy185 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy186 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0190 : nb068AlphaDummy183 ∈ (SemanticCore.Class.cv nb068AlphaDummy183).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy183).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0192 : nb068AlphaDummy125 ∈ (SemanticCore.Class.cv nb068AlphaDummy126).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy125).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0193 : nb068AlphaDummy125 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0194 (f : SemanticCore.Var) : nb068AlphaDummy127 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy128 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy127 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0195 (f : SemanticCore.Var) : nb068AlphaDummy127 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0196 : nb068AlphaDummy125 ∈ (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy168 (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0197 (f : SemanticCore.Var) : nb068AlphaDummy127 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy170 f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0198 : nb068AlphaDummy168 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0199 (f : SemanticCore.Var) : nb068AlphaDummy170 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0200 : nb068AlphaDummy168 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0201 (f : SemanticCore.Var) : nb068AlphaDummy170 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0202 : nb068AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb068AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb068AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))) Compiler.CompactSourceSyntax.synCid).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0204 : nb068AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb068AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0206 : nb068AlphaDummy000 ∈ (SemanticCore.Class.cv nb068AlphaDummy000).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0207 : nb068AlphaDummy000 ∈ {nb068AlphaDummy045} ∪ {nb068AlphaDummy046} ∪ (Compiler.CompactSourceSyntax.synWex nb068AlphaDummy047 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy045) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy047)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Class.cv nb068AlphaDummy000) (SemanticCore.Class.cv nb068AlphaDummy046)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0208 (f : SemanticCore.Var) : f ∈ (SemanticCore.Class.cv f).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0209 (f : SemanticCore.Var) : f ∈ {nb068AlphaDummy048 f} ∪ {nb068AlphaDummy049 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb068AlphaDummy050 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy048 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb068AlphaDummy050 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb068AlphaDummy049 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0210 : nb068AlphaDummy000 ∈ {nb068AlphaDummy125} ∪ {nb068AlphaDummy126} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Class.cv nb068AlphaDummy000) (SemanticCore.Class.cv nb068AlphaDummy125)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0211 (f : SemanticCore.Var) : f ∈ {nb068AlphaDummy127 f} ∪ {nb068AlphaDummy128 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb068AlphaDummy127 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0212 : nb068AlphaDummy000 ∈ (SemanticCore.Class.cv nb068AlphaDummy000).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0214 : nb068AlphaDummy047 ∈ (SemanticCore.Class.cv nb068AlphaDummy047).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy046).fv

Certificates from NAR4C068C001Part011.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0215 : nb068AlphaDummy047 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy203 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy204 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy203 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy204 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0216 (f : SemanticCore.Var) : nb068AlphaDummy050 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy050 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy049 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0217 (f : SemanticCore.Var) : nb068AlphaDummy050 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy205 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy206 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy205 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy206 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0218 : nb068AlphaDummy047 ∈ (SemanticCore.Class.cab nb068AlphaDummy203 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy204 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy203 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy204 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0219 (f : SemanticCore.Var) : nb068AlphaDummy050 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy205 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy206 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f)))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy205 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy206 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0220 : nb068AlphaDummy204 ∈ (SemanticCore.Class.cv nb068AlphaDummy204).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0221 (f : SemanticCore.Var) : nb068AlphaDummy206 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy206 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0223 (f : SemanticCore.Var) : nb068AlphaDummy213 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy213 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy213 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy213 f)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0226 : nb068AlphaDummy218 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy218) (SemanticCore.Class.cv nb068AlphaDummy219)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy218) (SemanticCore.Class.cv nb068AlphaDummy219)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0227 (f : SemanticCore.Var) : nb068AlphaDummy221 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy221 f)) (SemanticCore.Class.cv (nb068AlphaDummy222 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy221 f)) (SemanticCore.Class.cv (nb068AlphaDummy222 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0228 : nb068AlphaDummy218 ∈ (SemanticCore.Class.cv nb068AlphaDummy218).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy219).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0229 (f : SemanticCore.Var) : nb068AlphaDummy221 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy221 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy222 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0230 : nb068AlphaDummy219 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy218) (SemanticCore.Class.cv nb068AlphaDummy219)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy218) (SemanticCore.Class.cv nb068AlphaDummy219)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0231 (f : SemanticCore.Var) : nb068AlphaDummy222 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy221 f)) (SemanticCore.Class.cv (nb068AlphaDummy222 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy221 f)) (SemanticCore.Class.cv (nb068AlphaDummy222 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0232 : nb068AlphaDummy219 ∈ (SemanticCore.Class.cv nb068AlphaDummy218).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy219).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0233 (f : SemanticCore.Var) : nb068AlphaDummy222 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy221 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy222 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0234 : nb068AlphaDummy218 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy218)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy219)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0235 (f : SemanticCore.Var) : nb068AlphaDummy221 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy221 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy222 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0236 : nb068AlphaDummy218 ∈ (SemanticCore.Class.cv nb068AlphaDummy218).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy218).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0238 : nb068AlphaDummy219 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy218)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy219)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0239 (f : SemanticCore.Var) : nb068AlphaDummy222 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy221 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy222 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0240 : nb068AlphaDummy219 ∈ (SemanticCore.Class.cv nb068AlphaDummy219).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy219).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0242 : nb068AlphaDummy046 ∈ (SemanticCore.Class.cv nb068AlphaDummy047).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy046).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0243 : nb068AlphaDummy046 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy203 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy204 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy203 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy204 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0244 (f : SemanticCore.Var) : nb068AlphaDummy049 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy050 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy049 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0245 (f : SemanticCore.Var) : nb068AlphaDummy049 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy205 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy206 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy205 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy206 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0246 : nb068AlphaDummy046 ∈ (SemanticCore.Class.cab nb068AlphaDummy203 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy204 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy203 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy204 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy203) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0247 (f : SemanticCore.Var) : nb068AlphaDummy049 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy205 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy206 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy205 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy206 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy205 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0248 : nb068AlphaDummy204 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0249 (f : SemanticCore.Var) : nb068AlphaDummy206 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0250 : nb068AlphaDummy204 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy204)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0251 (f : SemanticCore.Var) : nb068AlphaDummy206 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy206 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0252 : nb068AlphaDummy240 ∈ (SemanticCore.Class.cv nb068AlphaDummy240).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy239).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0253 : nb068AlphaDummy240 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy243 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy244 (SemanticCore.Class.cv nb068AlphaDummy240) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy243 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy244 (SemanticCore.Class.cv nb068AlphaDummy239) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0254 (f : SemanticCore.Var) : nb068AlphaDummy242 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy242 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy241 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0255 (f : SemanticCore.Var) : nb068AlphaDummy242 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy245 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy246 f) (SemanticCore.Class.cv (nb068AlphaDummy242 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy245 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy246 f) (SemanticCore.Class.cv (nb068AlphaDummy241 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0256 : nb068AlphaDummy240 ∈ (SemanticCore.Class.cab nb068AlphaDummy243 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy244 (SemanticCore.Class.cv nb068AlphaDummy240) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy243 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy244 (SemanticCore.Class.cv nb068AlphaDummy240) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0257 (f : SemanticCore.Var) : nb068AlphaDummy242 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy245 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy246 f) (SemanticCore.Class.cv (nb068AlphaDummy242 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f)))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy245 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy246 f) (SemanticCore.Class.cv (nb068AlphaDummy242 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0258 : nb068AlphaDummy244 ∈ (SemanticCore.Class.cv nb068AlphaDummy244).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0259 (f : SemanticCore.Var) : nb068AlphaDummy246 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy246 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0261 (f : SemanticCore.Var) : nb068AlphaDummy253 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy253 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy253 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy253 f)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0264 : nb068AlphaDummy258 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy258) (SemanticCore.Class.cv nb068AlphaDummy259)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy258) (SemanticCore.Class.cv nb068AlphaDummy259)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0265 (f : SemanticCore.Var) : nb068AlphaDummy261 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy261 f)) (SemanticCore.Class.cv (nb068AlphaDummy262 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy261 f)) (SemanticCore.Class.cv (nb068AlphaDummy262 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0266 : nb068AlphaDummy258 ∈ (SemanticCore.Class.cv nb068AlphaDummy258).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy259).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0267 (f : SemanticCore.Var) : nb068AlphaDummy261 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy261 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy262 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0268 : nb068AlphaDummy259 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy258) (SemanticCore.Class.cv nb068AlphaDummy259)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy258) (SemanticCore.Class.cv nb068AlphaDummy259)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0269 (f : SemanticCore.Var) : nb068AlphaDummy262 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy261 f)) (SemanticCore.Class.cv (nb068AlphaDummy262 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy261 f)) (SemanticCore.Class.cv (nb068AlphaDummy262 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0270 : nb068AlphaDummy259 ∈ (SemanticCore.Class.cv nb068AlphaDummy258).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy259).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0271 (f : SemanticCore.Var) : nb068AlphaDummy262 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy261 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy262 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0272 : nb068AlphaDummy258 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy258)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy259)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0273 (f : SemanticCore.Var) : nb068AlphaDummy261 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy261 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy262 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0274 : nb068AlphaDummy258 ∈ (SemanticCore.Class.cv nb068AlphaDummy258).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy258).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0276 : nb068AlphaDummy259 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy258)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy259)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0277 (f : SemanticCore.Var) : nb068AlphaDummy262 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy261 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy262 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0278 : nb068AlphaDummy259 ∈ (SemanticCore.Class.cv nb068AlphaDummy259).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy259).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0280 : nb068AlphaDummy239 ∈ (SemanticCore.Class.cv nb068AlphaDummy240).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy239).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0281 : nb068AlphaDummy239 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy243 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy244 (SemanticCore.Class.cv nb068AlphaDummy240) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy243 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy244 (SemanticCore.Class.cv nb068AlphaDummy239) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0282 (f : SemanticCore.Var) : nb068AlphaDummy241 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy242 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy241 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0283 (f : SemanticCore.Var) : nb068AlphaDummy241 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy245 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy246 f) (SemanticCore.Class.cv (nb068AlphaDummy242 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy245 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy246 f) (SemanticCore.Class.cv (nb068AlphaDummy241 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0284 : nb068AlphaDummy239 ∈ (SemanticCore.Class.cab nb068AlphaDummy243 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy244 (SemanticCore.Class.cv nb068AlphaDummy239) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy243 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy244 (SemanticCore.Class.cv nb068AlphaDummy239) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy243) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0285 (f : SemanticCore.Var) : nb068AlphaDummy241 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy245 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy246 f) (SemanticCore.Class.cv (nb068AlphaDummy241 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy245 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy246 f) (SemanticCore.Class.cv (nb068AlphaDummy241 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy245 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0286 : nb068AlphaDummy244 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0287 (f : SemanticCore.Var) : nb068AlphaDummy246 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0288 : nb068AlphaDummy244 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy244)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0289 (f : SemanticCore.Var) : nb068AlphaDummy246 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy246 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0290 : nb068AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0291 (f : SemanticCore.Var) : f ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0292 : nb068AlphaDummy284 ∈ (SemanticCore.Class.cv nb068AlphaDummy284).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy283).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0293 : nb068AlphaDummy284 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy287 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy284) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy287 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy283) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0294 (f : SemanticCore.Var) : nb068AlphaDummy286 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy286 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy285 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0295 (f : SemanticCore.Var) : nb068AlphaDummy286 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy289 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy286 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy289 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy285 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0296 : nb068AlphaDummy284 ∈ (SemanticCore.Class.cab nb068AlphaDummy287 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy284) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy287 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy284) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0297 (f : SemanticCore.Var) : nb068AlphaDummy286 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy289 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy286 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f)))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy289 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy286 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0298 : nb068AlphaDummy288 ∈ (SemanticCore.Class.cv nb068AlphaDummy288).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0299 (f : SemanticCore.Var) : nb068AlphaDummy290 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy290 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0301 (f : SemanticCore.Var) : nb068AlphaDummy297 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy297 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy297 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy297 f)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0304 : nb068AlphaDummy302 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy302) (SemanticCore.Class.cv nb068AlphaDummy303)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy302) (SemanticCore.Class.cv nb068AlphaDummy303)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0305 (f : SemanticCore.Var) : nb068AlphaDummy305 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy305 f)) (SemanticCore.Class.cv (nb068AlphaDummy306 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy305 f)) (SemanticCore.Class.cv (nb068AlphaDummy306 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0306 : nb068AlphaDummy302 ∈ (SemanticCore.Class.cv nb068AlphaDummy302).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy303).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0307 (f : SemanticCore.Var) : nb068AlphaDummy305 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy305 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy306 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0308 : nb068AlphaDummy303 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy302) (SemanticCore.Class.cv nb068AlphaDummy303)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy302) (SemanticCore.Class.cv nb068AlphaDummy303)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0309 (f : SemanticCore.Var) : nb068AlphaDummy306 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy305 f)) (SemanticCore.Class.cv (nb068AlphaDummy306 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy305 f)) (SemanticCore.Class.cv (nb068AlphaDummy306 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0310 : nb068AlphaDummy303 ∈ (SemanticCore.Class.cv nb068AlphaDummy302).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy303).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0311 (f : SemanticCore.Var) : nb068AlphaDummy306 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy305 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy306 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0312 : nb068AlphaDummy302 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy302)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy303)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0313 (f : SemanticCore.Var) : nb068AlphaDummy305 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy305 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy306 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0314 : nb068AlphaDummy302 ∈ (SemanticCore.Class.cv nb068AlphaDummy302).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy302).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0316 : nb068AlphaDummy303 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy302)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy303)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0317 (f : SemanticCore.Var) : nb068AlphaDummy306 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy305 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy306 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0318 : nb068AlphaDummy303 ∈ (SemanticCore.Class.cv nb068AlphaDummy303).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy303).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0320 : nb068AlphaDummy283 ∈ (SemanticCore.Class.cv nb068AlphaDummy284).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy283).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0321 : nb068AlphaDummy283 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy287 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy284) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy287 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy283) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0322 (f : SemanticCore.Var) : nb068AlphaDummy285 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy286 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy285 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0323 (f : SemanticCore.Var) : nb068AlphaDummy285 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy289 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy286 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy289 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy285 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0324 : nb068AlphaDummy283 ∈ (SemanticCore.Class.cab nb068AlphaDummy287 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy283) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy287 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy283) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0325 (f : SemanticCore.Var) : nb068AlphaDummy285 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy289 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy285 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy289 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy285 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0326 : nb068AlphaDummy288 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0327 (f : SemanticCore.Var) : nb068AlphaDummy290 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0328 : nb068AlphaDummy288 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0329 (f : SemanticCore.Var) : nb068AlphaDummy290 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0330 : nb068AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy002)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy002)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0331 (y f : SemanticCore.Var) : f ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv y)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0332 : nb068AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb068AlphaDummy000)).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0333 (y f : SemanticCore.Var) : f ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0334 : nb068AlphaDummy000 ∈ (SemanticCore.Class.cv nb068AlphaDummy000).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0335 (f : SemanticCore.Var) : f ∈ (SemanticCore.Class.cv f).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0336 : nb068AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy002)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy002)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0337 (y f : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv y)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0338 : nb068AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb068AlphaDummy000)).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0339 (y f : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0340 : nb068AlphaDummy327 ∈ {nb068AlphaDummy327} ∪ {nb068AlphaDummy328} ∪ (Compiler.CompactSourceSyntax.synWex nb068AlphaDummy329 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy327) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))) (SemanticCore.Class.cv nb068AlphaDummy329)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy329) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy328)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0341 (f : SemanticCore.Var) : nb068AlphaDummy330 f ∈ {nb068AlphaDummy330 f} ∪ {nb068AlphaDummy331 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb068AlphaDummy332 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy330 f)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (nb068AlphaDummy332 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy332 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb068AlphaDummy331 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0342 : nb068AlphaDummy328 ∈ {nb068AlphaDummy327} ∪ {nb068AlphaDummy328} ∪ (Compiler.CompactSourceSyntax.synWex nb068AlphaDummy329 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy327) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))) (SemanticCore.Class.cv nb068AlphaDummy329)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy329) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy328)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0343 (f : SemanticCore.Var) : nb068AlphaDummy331 f ∈ {nb068AlphaDummy330 f} ∪ {nb068AlphaDummy331 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb068AlphaDummy332 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy330 f)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (nb068AlphaDummy332 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy332 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb068AlphaDummy331 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0344 : nb068AlphaDummy327 ∈ (SemanticCore.Class.cv nb068AlphaDummy327).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy328).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0345 : nb068AlphaDummy327 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy335 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy336 (SemanticCore.Class.cv nb068AlphaDummy327) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy335 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy336 (SemanticCore.Class.cv nb068AlphaDummy328) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0346 (f : SemanticCore.Var) : nb068AlphaDummy330 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy330 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy331 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0347 (f : SemanticCore.Var) : nb068AlphaDummy330 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy337 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy338 f) (SemanticCore.Class.cv (nb068AlphaDummy330 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy337 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy338 f) (SemanticCore.Class.cv (nb068AlphaDummy331 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0348 : nb068AlphaDummy327 ∈ (SemanticCore.Class.cab nb068AlphaDummy335 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy336 (SemanticCore.Class.cv nb068AlphaDummy327) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy335 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy336 (SemanticCore.Class.cv nb068AlphaDummy327) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0349 (f : SemanticCore.Var) : nb068AlphaDummy330 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy337 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy338 f) (SemanticCore.Class.cv (nb068AlphaDummy330 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f)))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy337 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy338 f) (SemanticCore.Class.cv (nb068AlphaDummy330 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0350 : nb068AlphaDummy336 ∈ (SemanticCore.Class.cv nb068AlphaDummy336).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0351 (f : SemanticCore.Var) : nb068AlphaDummy338 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy338 f)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0353 (f : SemanticCore.Var) : nb068AlphaDummy345 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy345 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy345 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy345 f)).fv

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

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