NF weak partition development: NominalAlphaOprabCompactCertificate001.

The equality branches in the nominal batch source are unnecessary here: the three inner binders are paired with themselves, while only the outer fresh binder is renamed. This certificate therefore works uniformly even when any of x, y, and z coincide.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb049OprabAlphaCertificate (ph : SemanticCore.Wff) (x y z w : SemanticCore.Var) (dv_ph_w : w ∉ ph.fv) (dv_w_x : w ≠ x) (dv_w_y : w ≠ y) (dv_w_z : w ≠ z) : Nominal.TAlphaClass [] (Compiler.CompactSourceSyntax.synCoprab x y z ph) (SemanticCore.Class.cab w (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv w) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv z))) ph)))))

Checked nominal proof certificate identified upstream as nb049_oprab_alpha_certificate.

Equations

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