NF weak partition development: NominalAlphaRepairedBase001003V.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfV (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCvv (SemanticCore.Class.cab x (SemanticCore.Wff.objEq x x)))

Checked nominal proof certificate identified upstream as nominal_df_v.

Equations

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