NF weak partition development: NAR4H5C095M3Part020.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095WppRefl0116 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_S_f : f ∉ S_cls.fv) (dv_S_u : u ∉ S_cls.fv) (dv_S_x : x ∉ S_cls.fv) : Nominal.TReflOn [(nb095AlphaDummy340 D R S_cls E, nb095AlphaDummy342 u S_cls), (nb095AlphaDummy339 D R S_cls E, nb095AlphaDummy341 u S_cls), (nb095AlphaDummy337 D R S_cls E, nb095AlphaDummy338 u S_cls E), (nb095AlphaDummy335 D R S_cls E, nb095AlphaDummy336 u S_cls E), (nb095AlphaDummy293 D R S_cls E, nb095AlphaDummy294 u S_cls f E), (nb095AlphaDummy291 D R S_cls E, nb095AlphaDummy292 u S_cls f E), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

Checked nominal proof certificate identified upstream as nb095_wpp_refl_0116.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095WppRefl0116 x u D R S_cls f E dv_S_f dv_S_u dv_S_x = ⋯.reflOn