NF weak partition development: NominalAlphaRepairedBase001030Oddfin.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfOddfin
(x n : SemanticCore.Var)
(dv_n_x : n ≠ x)
:
Nominal.NPrf
(SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCoddfin
(SemanticCore.Class.cab x
(Compiler.CompactSourceSyntax.synWa
(Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc
(SemanticCore.Wff.classEq (SemanticCore.Class.cv x)
(Compiler.CompactSourceSyntax.synCplc
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) (SemanticCore.Class.cv n))
Compiler.CompactSourceSyntax.synC1c)))
(Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC0))))
Checked nominal proof certificate identified upstream as nominal_df_oddfin.
Equations
- One or more equations did not get rendered due to their size.