NF weak partition development: NAR4H5C093M3Part005.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093WppRefl0029 (A : SemanticCore.Class) (r d : SemanticCore.Var) : Nominal.TReflOn [(nb093AlphaDummy000 A, d), (nb093AlphaDummy001 A, r), (nb093AlphaDummy006 A, nb093AlphaDummy007 r d), (nb093AlphaDummy004 A, nb093AlphaDummy005 A r d), (nb093AlphaDummy002 A, nb093AlphaDummy003 A r d)] Compiler.CompactSourceSyntax.synCfound.fv

Checked nominal proof certificate identified upstream as nb093_wpp_refl_0029.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093WppRefl0029 A r d = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfLnpwc (A : SemanticCore.Class) (r d : SemanticCore.Var) (__dv_A_d : d ∉ A.fv) (__dv_A_r : r ∉ A.fv) (dv_d_r : d ≠ r) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synClnpwc A) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synClntpc A) (Compiler.CompactSourceSyntax.synCopab r d (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r))) Compiler.CompactSourceSyntax.synCfound (SemanticCore.Class.cv d)))))

Checked nominal proof certificate identified upstream as nominal_df_lnpwc.

Equations

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