NF weak partition development: NominalWPPReplayChunk010Compact001Part006.
noncomputable def
NFChoice.DirectNominalPrf.WPPReplay.gNnadjoinlem1
(x y n b l : SemanticCore.Var)
(dv_b_l : b ≠ l)
(_dv_b_n : b ≠ n)
(dv_b_x : b ≠ x)
(dv_b_y : b ≠ y)
(dv_l_n : l ≠ n)
(dv_l_x : l ≠ x)
(dv_l_y : l ≠ 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 l (SemanticCore.Class.cv n)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv y)
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv l)))).imp
(SemanticCore.Wff.classMem
(SemanticCore.Class.cab x
(Compiler.CompactSourceSyntax.synWrex b (SemanticCore.Class.cv l)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv x)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv b)
(Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))))))
(SemanticCore.Class.cv n)))))
Compiler.CompactSourceSyntax.synCvv)
Checked nominal proof certificate identified upstream as g_nnadjoinlem1.
Equations
- One or more equations did not get rendered due to their size.