NF weak partition development: NominalAlphaRepairedBase001022Iota.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfIota (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCio x ph) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cab y (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ph) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as nominal_df_iota.

Equations

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