Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part018.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSfinltfin (P Q M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWsfin M N) (Compiler.CompactSourceSyntax.synWsfin P Q)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk M P) Compiler.CompactSourceSyntax.synCltfin)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk N Q) Compiler.CompactSourceSyntax.synCltfin))

Checked nominal proof certificate identified upstream as g_sfinltfin.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part019.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSfin111 (P M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWsfin M P) (Compiler.CompactSourceSyntax.synWsfin N P)).imp (SemanticCore.Wff.classEq M N))

Checked nominal proof certificate identified upstream as g_sfin111.

Equations

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