Documentation

LeanPool.NFWeakPartition.NominalAlphaRepairedBase001036Proj2Reflected001

NF weak partition development: NominalAlphaRepairedBase001036Proj2Reflected001.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfProj2 (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :
Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCproj2 A) (SemanticCore.Class.cab x (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) A)))

Checked nominal proof certificate identified upstream as nominal_df_proj2.

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