Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part015.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSfintfin (M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWsfin M N).imp (Compiler.CompactSourceSyntax.synWsfin (Compiler.CompactSourceSyntax.synCtfin M) (Compiler.CompactSourceSyntax.synCtfin N)))

Checked nominal proof certificate identified upstream as g_sfintfin.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part016.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfinnnlem1 (x y n a : SemanticCore.Var) (_dv_a_n : a ≠ n) (dv_a_x : a ≠ x) (dv_a_y : a ≠ y) (_dv_n_x : n ≠ x) (dv_n_y : n ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab n (Compiler.CompactSourceSyntax.synWral y (SemanticCore.Class.cv n) ((Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cab a (Compiler.CompactSourceSyntax.synWrex x (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv a) (Compiler.CompactSourceSyntax.synCtfin (SemanticCore.Class.cv x))))) (Compiler.CompactSourceSyntax.synCtfin (SemanticCore.Class.cv n)))))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_tfinnnlem1.

Equations

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