NF weak partition development: NAR4C076C001Part013.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076WppRefl0029 (g m n a b : SemanticCore.Var) : Nominal.TReflOn [(nb076AlphaDummy002, g), (nb076AlphaDummy001, b), (nb076AlphaDummy000, a), (nb076AlphaDummy005, nb076AlphaDummy006 g m n a b), (nb076AlphaDummy004, n), (nb076AlphaDummy003, m), (nb076AlphaDummy007, nb076AlphaDummy008 g m n a b)] Compiler.CompactSourceSyntax.synCen.fv

Checked nominal proof certificate identified upstream as nb076_wpp_refl_0029.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076WppRefl0029 g m n a b = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfMuc (g m n a b : SemanticCore.Var) (dv_a_b : a ≠ b) (dv_a_g : a ≠ g) (dv_a_m : a ≠ m) (dv_a_n : a ≠ n) (dv_b_g : b ≠ g) (dv_b_m : b ≠ m) (dv_b_n : b ≠ n) (__dv_g_m : g ≠ m) (dv_g_n : g ≠ n) (dv_m_n : m ≠ n) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCmuc (Compiler.CompactSourceSyntax.synCmpt2 m Compiler.CompactSourceSyntax.synCncs n Compiler.CompactSourceSyntax.synCncs (SemanticCore.Class.cab a (Compiler.CompactSourceSyntax.synWrex b (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synWrex g (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv a) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv b) (SemanticCore.Class.cv g))))))))

Checked nominal proof certificate identified upstream as nominal_df_muc.

Equations

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