NF weak partition development: NominalAlphaRepairedBase001025Lefin.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfLefin (x y z w : SemanticCore.Var) (__dv_w_x : w ≠ x) (dv_w_y : w ≠ y) (dv_w_z : w ≠ z) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synClefin (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))) (Compiler.CompactSourceSyntax.synWrex w Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv y) (SemanticCore.Class.cv w)))))))))

Checked nominal proof certificate identified upstream as nominal_df_lefin.

Equations

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