NF weak partition development: NAR4C052C001Part003.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb052_support_mem_0087 (x y : SemanticCore.Var) : nb052AlphaDummy003 x y ∈ (SemanticCore.Class.cab (nb052AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb052AlphaDummy009 x y) (SemanticCore.Class.cv (nb052AlphaDummy003 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb052AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb052AlphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb052AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb052AlphaDummy009 x y) (SemanticCore.Class.cv (nb052AlphaDummy003 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb052AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb052AlphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb052_support_mem_0089 (x y : SemanticCore.Var) : nb052AlphaDummy009 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb052AlphaDummy009 x y)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb052_support_mem_0091 (x y : SemanticCore.Var) : nb052AlphaDummy009 x y ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb052AlphaDummy009 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb052AlphaDummy009 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb052_support_mem_0092 : nb052AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb052AlphaDummy000)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb052AlphaDummy001)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb052_support_mem_0093 (x y : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv x)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb052_support_mem_0094 : nb052AlphaDummy000 ∈ (SemanticCore.Class.cv nb052AlphaDummy000).fv ∪ (SemanticCore.Class.cv nb052AlphaDummy000).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb052_support_mem_0095 (x : SemanticCore.Var) : x ∈ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv x).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb052_support_mem_0096 : nb052AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb052AlphaDummy000)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb052AlphaDummy001)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb052_support_mem_0097 (x y : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv x)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb052_support_mem_0098 : nb052AlphaDummy001 ∈ (SemanticCore.Class.cv nb052AlphaDummy001).fv ∪ (SemanticCore.Class.cv nb052AlphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb052_support_mem_0099 (y : SemanticCore.Var) : y ∈ (SemanticCore.Class.cv y).fv ∪ (SemanticCore.Class.cv y).fv