NF weak partition development: NominalWPPReplayChunk010Compact001Part009.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnpweqlem1 (m n a b : SemanticCore.Var) (dv_a_b : a ≠ b) (dv_a_m : a ≠ m) (dv_a_n : a ≠ n) (dv_b_m : b ≠ m) (dv_b_n : b ≠ n) (_dv_m_n : m ≠ n) : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab m (Compiler.CompactSourceSyntax.synWral a (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synWral b (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv a)) (SemanticCore.Class.cv n)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw (SemanticCore.Class.cv b)) (SemanticCore.Class.cv n))))))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_nnpweqlem1.

Equations

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