NF weak partition development: NominalAlphaRepairedBase001031Sfin.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfSfin (M N : SemanticCore.Class) (a : SemanticCore.Var) (dv_M_a : a ∉ M.fv) (dv_N_a : a ∉ N.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsfin M N) (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWex a (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) M) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv a)) N)))))

Checked nominal proof certificate identified upstream as nominal_df_sfin.

Equations

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