Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part056.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCoexg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCcom A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_coexg.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part057.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCoex (A B : SemanticCore.Class) (hyp_coex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_coex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCcom A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_coex.

Equations

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