NF weak partition development: NominalAlphaRepairedBase001032Spfin.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfSpfin (x z a : SemanticCore.Var) (dv_a_x : a ≠ x) (dv_a_z : a ≠ z) (dv_x_z : x ≠ z) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCspfin (Compiler.CompactSourceSyntax.synCint (SemanticCore.Class.cab a (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCncfin Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Class.cv a)) (Compiler.CompactSourceSyntax.synWral x (SemanticCore.Class.cv a) (SemanticCore.Wff.all z ((Compiler.CompactSourceSyntax.synWsfin (SemanticCore.Class.cv z) (SemanticCore.Class.cv x)).imp (SemanticCore.Wff.objMem z a))))))))

Checked nominal proof certificate identified upstream as nominal_df_spfin.

Equations

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