Documentation

LeanPool.NFWeakPartition.NAR4H5C091M3BPart003

NF weak partition development: NAR4H5C091M3BPart003.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091SplitAlpha0000 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
Nominal.TAlphaWff [(nb091AlphaDummy035 D R, nb091AlphaDummy036 D R p), (nb091AlphaDummy009 D R, nb091AlphaDummy010 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy035 D R)) (SemanticCore.Class.cab (nb091AlphaDummy005 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy006 D R) (SemanticCore.Class.cv (nb091AlphaDummy001 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy005 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy036 D R p)) (SemanticCore.Class.cab (nb091AlphaDummy007 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy008 D R p) (SemanticCore.Class.cv (nb091AlphaDummy002 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy007 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg

Checked nominal proof certificate identified upstream as nb091_split_alpha_0000.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091SplitAlpha0001 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb091AlphaDummy035 D R, nb091AlphaDummy036 D R p), (nb091AlphaDummy009 D R, nb091AlphaDummy010 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy035 D R)) (SemanticCore.Class.cab (nb091AlphaDummy005 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy006 D R) (SemanticCore.Class.cv (nb091AlphaDummy001 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy005 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy035 D R)) (SemanticCore.Class.cab (nb091AlphaDummy005 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy006 D R) (SemanticCore.Class.cv (nb091AlphaDummy001 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy005 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy006 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy036 D R p)) (SemanticCore.Class.cab (nb091AlphaDummy007 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy008 D R p) (SemanticCore.Class.cv (nb091AlphaDummy002 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy007 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy036 D R p)) (SemanticCore.Class.cab (nb091AlphaDummy007 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy008 D R p) (SemanticCore.Class.cv (nb091AlphaDummy002 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy007 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy008 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

    Checked nominal proof certificate identified upstream as nb091_split_alpha_0001.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091SplitAlpha0002 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy003 D R)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb091AlphaDummy000 D R)) (SemanticCore.Class.cv (nb091AlphaDummy001 D R)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy004 D R p)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv p) (SemanticCore.Class.cv (nb091AlphaDummy002 D R p))))

      Checked nominal proof certificate identified upstream as nb091_split_alpha_0002.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0000 (D R : SemanticCore.Class) :
        nb091AlphaDummy001 D R ∉ D.fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0106 (D R : SemanticCore.Class) :
        nb091AlphaDummy001 D R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0001 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
        nb091AlphaDummy002 D R p ∉ D.fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0107 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
        nb091AlphaDummy002 D R p ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0002 (D R : SemanticCore.Class) :
        nb091AlphaDummy000 D R ∉ D.fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0108 (D R : SemanticCore.Class) :
        nb091AlphaDummy000 D R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0109 (D : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) :
        p ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0003 (D R : SemanticCore.Class) :
        nb091AlphaDummy003 D R ∉ D.fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0110 (D R : SemanticCore.Class) :
        nb091AlphaDummy003 D R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0004 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
        nb091AlphaDummy004 D R p ∉ D.fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0111 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
        nb091AlphaDummy004 D R p ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv
        source
        theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_envfresh_0007 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) :
        Nominal.TEnvFresh [(nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv
        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091WppRefl0007 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) :
        Nominal.TReflOn [(nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)).fv

        Checked nominal proof certificate identified upstream as nb091_wpp_refl_0007.

        Equations
        Instances For
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0005 (D R : SemanticCore.Class) :
          nb091AlphaDummy057 D R ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0006 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
          nb091AlphaDummy058 D R p ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0007 (D R : SemanticCore.Class) :
          nb091AlphaDummy055 D R ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0008 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
          nb091AlphaDummy056 D R p ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0009 (D R : SemanticCore.Class) :
          nb091AlphaDummy048 D R ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0010 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
          nb091AlphaDummy050 D R p ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0011 (D R : SemanticCore.Class) :
          nb091AlphaDummy047 D R ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0012 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
          nb091AlphaDummy049 D R p ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0013 (D R : SemanticCore.Class) :
          nb091AlphaDummy053 D R ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0014 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
          nb091AlphaDummy054 D R p ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0015 (D R : SemanticCore.Class) :
          nb091AlphaDummy051 D R ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0016 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
          nb091AlphaDummy052 D R p ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0017 (D R : SemanticCore.Class) :
          nb091AlphaDummy045 D R ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0018 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
          nb091AlphaDummy046 D R p ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0019 (D R : SemanticCore.Class) :
          nb091AlphaDummy042 D R ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0020 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
          nb091AlphaDummy044 D R p ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0021 (D R : SemanticCore.Class) :
          nb091AlphaDummy041 D R ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0022 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
          nb091AlphaDummy043 D R p ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0023 (D R : SemanticCore.Class) :
          nb091AlphaDummy001 D R ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0024 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
          nb091AlphaDummy002 D R p ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0025 (D R : SemanticCore.Class) :
          nb091AlphaDummy000 D R ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0026 (D R : SemanticCore.Class) :
          nb091AlphaDummy003 D R ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0027 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
          nb091AlphaDummy004 D R p ∉ R.fv
          source
          theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_envfresh_0008 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_R_p : p ∉ R.fv) :
          Nominal.TEnvFresh [(nb091AlphaDummy057 D R, nb091AlphaDummy058 D R p), (nb091AlphaDummy055 D R, nb091AlphaDummy056 D R p), (nb091AlphaDummy048 D R, nb091AlphaDummy050 D R p), (nb091AlphaDummy047 D R, nb091AlphaDummy049 D R p), (nb091AlphaDummy053 D R, nb091AlphaDummy054 D R p), (nb091AlphaDummy051 D R, nb091AlphaDummy052 D R p), (nb091AlphaDummy045 D R, nb091AlphaDummy046 D R p), (nb091AlphaDummy042 D R, nb091AlphaDummy044 D R p), (nb091AlphaDummy041 D R, nb091AlphaDummy043 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] R.fv
          source
          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091FocusedRefl0000 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_R_p : p ∉ R.fv) :
          Nominal.TReflOn [(nb091AlphaDummy057 D R, nb091AlphaDummy058 D R p), (nb091AlphaDummy055 D R, nb091AlphaDummy056 D R p), (nb091AlphaDummy048 D R, nb091AlphaDummy050 D R p), (nb091AlphaDummy047 D R, nb091AlphaDummy049 D R p), (nb091AlphaDummy053 D R, nb091AlphaDummy054 D R p), (nb091AlphaDummy051 D R, nb091AlphaDummy052 D R p), (nb091AlphaDummy045 D R, nb091AlphaDummy046 D R p), (nb091AlphaDummy042 D R, nb091AlphaDummy044 D R p), (nb091AlphaDummy041 D R, nb091AlphaDummy043 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)] R.fv

          Checked nominal proof certificate identified upstream as nb091_focused_refl_0000.

          Equations
          Instances For
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0052 (D R : SemanticCore.Class) :
            nb091AlphaDummy060 D R ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0053 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
            nb091AlphaDummy062 D R p ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0054 (D R : SemanticCore.Class) :
            nb091AlphaDummy059 D R ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0055 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
            nb091AlphaDummy061 D R p ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0056 (D R : SemanticCore.Class) :
            nb091AlphaDummy063 D R ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0057 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
            nb091AlphaDummy064 D R p ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0058 (D R : SemanticCore.Class) :
            nb091AlphaDummy057 D R ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0059 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
            nb091AlphaDummy058 D R p ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0060 (D R : SemanticCore.Class) :
            nb091AlphaDummy055 D R ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0061 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
            nb091AlphaDummy056 D R p ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0062 (D R : SemanticCore.Class) :
            nb091AlphaDummy048 D R ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0063 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
            nb091AlphaDummy050 D R p ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0064 (D R : SemanticCore.Class) :
            nb091AlphaDummy047 D R ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0065 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
            nb091AlphaDummy049 D R p ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0066 (D R : SemanticCore.Class) :
            nb091AlphaDummy053 D R ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0067 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
            nb091AlphaDummy054 D R p ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0068 (D R : SemanticCore.Class) :
            nb091AlphaDummy051 D R ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0069 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
            nb091AlphaDummy052 D R p ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0070 (D R : SemanticCore.Class) :
            nb091AlphaDummy045 D R ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0071 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
            nb091AlphaDummy046 D R p ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0072 (D R : SemanticCore.Class) :
            nb091AlphaDummy042 D R ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0073 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
            nb091AlphaDummy044 D R p ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0074 (D R : SemanticCore.Class) :
            nb091AlphaDummy041 D R ∉ ∅
            source
            theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_fv_empty_0075 (D R : SemanticCore.Class) (p : SemanticCore.Var) :
            nb091AlphaDummy043 D R p ∉ ∅