NF weak partition development: NominalWPPReplayChunk010Compact001Part017.
noncomputable def
NFChoice.DirectNominalPrf.WPPReplay.gTfinnn
(x : SemanticCore.Var)
(A N : SemanticCore.Class)
(a : SemanticCore.Var)
(dv_A_a : a ∉ A.fv)
(dv_A_x : x ∉ A.fv)
(_dv_N_a : a ∉ N.fv)
(_dv_N_x : x ∉ N.fv)
(dv_a_x : a ≠ x)
:
Nominal.NPrf
((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)
(Compiler.CompactSourceSyntax.synWss A Compiler.CompactSourceSyntax.synCnnc)
(SemanticCore.Wff.classMem A N)).imp
(SemanticCore.Wff.classMem
(SemanticCore.Class.cab a
(Compiler.CompactSourceSyntax.synWrex x A
(SemanticCore.Wff.classEq (SemanticCore.Class.cv a)
(Compiler.CompactSourceSyntax.synCtfin (SemanticCore.Class.cv x)))))
(Compiler.CompactSourceSyntax.synCtfin N)))
Checked nominal proof certificate identified upstream as g_tfinnn.
Equations
- One or more equations did not get rendered due to their size.