NF weak partition development: NAR4H5C096M3Part004.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096WppRefl0023 (D R : SemanticCore.Class) (q : SemanticCore.Var) : Nominal.TReflOn [(nb096AlphaDummy042 D R, nb096AlphaDummy044 D R q), (nb096AlphaDummy041 D R, nb096AlphaDummy043 D R q), (nb096AlphaDummy001 D R, nb096AlphaDummy002 D R q), (nb096AlphaDummy000 D R, q), (nb096AlphaDummy003 D R, nb096AlphaDummy004 D R q)] Compiler.CompactSourceSyntax.synCen.fv

Checked nominal proof certificate identified upstream as nb096_wpp_refl_0023.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096WppRefl0023 D R q = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfWecutcardfn (D R : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_q : q ∉ D.fv) (dv_R_q : q ∉ R.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCwecutcardfn R D) (Compiler.CompactSourceSyntax.synCmpt q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))))))))

Checked nominal proof certificate identified upstream as nominal_df_wecutcardfn.

Equations

• One or more equations did not get rendered due to their size.