NF weak partition development: NominalWPPReplayChunk009StructuralPart058.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEvenfinex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCevenfin Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_evenfinex.

Equations

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