NF weak partition development: NominalAlphaRepairedBase001047FvReflected001.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfFv (x : SemanticCore.Var) (A F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_F_x : x ∉ F.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCio x (Compiler.CompactSourceSyntax.synWbr A F (SemanticCore.Class.cv x))))

Checked nominal proof certificate identified upstream as nominal_df_fv.

Equations

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