NF weak partition development: NominalAlphaRepairedBase001026Ltfin.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfLtfin (x m n p : SemanticCore.Var) (dv_m_n : m ≠ n) (dv_m_p : m ≠ p) (dv_m_x : m ≠ x) (dv_n_p : n ≠ p) (dv_n_x : n ≠ x) (__dv_p_x : p ≠ x) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCltfin (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWex m (Compiler.CompactSourceSyntax.synWex n (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv m) (SemanticCore.Class.cv n))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWrex p Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv m) (SemanticCore.Class.cv p)) Compiler.CompactSourceSyntax.synC1c)))))))))

Checked nominal proof certificate identified upstream as nominal_df_ltfin.

Equations

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