NF weak partition development: NominalAlphaRepairedBase001035Proj1Reflected001.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfProj1 (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCproj1 A) (SemanticCore.Class.cab x (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv x)) A)))

Checked nominal proof certificate identified upstream as nominal_df_proj1.

Equations

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