NF weak partition development: NominalWPPReplayChunk006.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcrd (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) (hyp_nfeqd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A)))

Checked nominal proof certificate identified upstream as g_nfcrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfeqd (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfeqd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))) (hyp_nfeqd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_nfeqd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfeld (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfeqd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))) (hyp_nfeqd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.classMem A B)))

Checked nominal proof certificate identified upstream as g_nfeld.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDrnfc1 (x y : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_drnfc1_1 : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWnfc x A) (Compiler.CompactSourceSyntax.synWnfc y B)))

Checked nominal proof certificate identified upstream as g_drnfc1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfabd2 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfabd2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_nfabd2_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg).imp (Compiler.CompactSourceSyntax.synWnf x ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x (SemanticCore.Class.cab y ps)))

Checked nominal proof certificate identified upstream as g_nfabd2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfabd (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfabd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_nfabd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x (SemanticCore.Class.cab y ps)))

Checked nominal proof certificate identified upstream as g_nfabd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDvelimdc (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_dvelimdc_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_dvelimdc_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z ph)) (hyp_dvelimdc_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))) (hyp_dvelimdc_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc z B))) (hyp_dvelimdc_5 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.objEq z y).imp (SemanticCore.Wff.classEq A B)))) : Nominal.NPrf (ph.imp ((SemanticCore.Wff.all x (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).neg.imp (Compiler.CompactSourceSyntax.synWnfc x B)))

Checked nominal proof certificate identified upstream as g_dvelimdc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDvelimc (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_dvelimc_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_dvelimc_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc z B)) (hyp_dvelimc_3 : Nominal.NPrf ((SemanticCore.Wff.objEq z y).imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).neg.imp (Compiler.CompactSourceSyntax.synWnfc x B))

Checked nominal proof certificate identified upstream as g_dvelimc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcvf (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).neg.imp (Compiler.CompactSourceSyntax.synWnfc x (SemanticCore.Class.cv y)))

Checked nominal proof certificate identified upstream as g_nfcvf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCleqf (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_cleqf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_cleqf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B))))

Checked nominal proof certificate identified upstream as g_cleqf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNne (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne A B).neg (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_nne.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNeirr (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne A A).neg

Checked nominal proof certificate identified upstream as g_neirr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNeeq1 (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne A C) (Compiler.CompactSourceSyntax.synWne B C)))

Checked nominal proof certificate identified upstream as g_neeq1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNeeq2 (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne C A) (Compiler.CompactSourceSyntax.synWne C B)))

Checked nominal proof certificate identified upstream as g_neeq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNeeq1i (A B C : SemanticCore.Class) (hyp_neeq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne A C) (Compiler.CompactSourceSyntax.synWne B C))

Checked nominal proof certificate identified upstream as g_neeq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNeeq1i A B C hyp_neeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_neeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gNeeq1 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNeeq2i (A B C : SemanticCore.Class) (hyp_neeq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne C A) (Compiler.CompactSourceSyntax.synWne C B))

Checked nominal proof certificate identified upstream as g_neeq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNeeq2i A B C hyp_neeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_neeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gNeeq2 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNeeq1d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_neeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne A C) (Compiler.CompactSourceSyntax.synWne B C)))

Checked nominal proof certificate identified upstream as g_neeq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNeeq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_neeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne C A) (Compiler.CompactSourceSyntax.synWne C B)))

Checked nominal proof certificate identified upstream as g_neeq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNeeq12d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_neeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_neeq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne A C) (Compiler.CompactSourceSyntax.synWne B D)))

Checked nominal proof certificate identified upstream as g_neeq12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNeneqd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_neneqd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWne A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B).neg)

Checked nominal proof certificate identified upstream as g_neneqd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqnetri (A B C : SemanticCore.Class) (hyp_eqnetr_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_eqnetr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne B C)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne A C)

Checked nominal proof certificate identified upstream as g_eqnetri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqnetrd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eqnetrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqnetrd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWne B C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWne A C))

Checked nominal proof certificate identified upstream as g_eqnetrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqnetrri (A B C : SemanticCore.Class) (hyp_eqnetrr_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_eqnetrr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne A C)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne B C)

Checked nominal proof certificate identified upstream as g_eqnetrri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqnetrrd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eqnetrrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqnetrrd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWne A C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWne B C))

Checked nominal proof certificate identified upstream as g_eqnetrrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon3abii (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon3abii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A B) ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne A B) ph.neg)

Checked nominal proof certificate identified upstream as g_necon3abii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon3bbii (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon3bbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph.neg (Compiler.CompactSourceSyntax.synWne A B))

Checked nominal proof certificate identified upstream as g_necon3bbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon3bii (A B C D : SemanticCore.Class) (hyp_necon3bii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne A B) (Compiler.CompactSourceSyntax.synWne C D))

Checked nominal proof certificate identified upstream as g_necon3bii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon3abid (ph ps : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon3abid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A B) ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne A B) ps.neg))

Checked nominal proof certificate identified upstream as g_necon3abid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon3bbid (ph ps : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon3bbid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps (SemanticCore.Wff.classEq A B)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps.neg (Compiler.CompactSourceSyntax.synWne A B)))

Checked nominal proof certificate identified upstream as g_necon3bbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon3ad (ph ps : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon3ad_1 : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.classEq A B)))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWne A B).imp ps.neg))

Checked nominal proof certificate identified upstream as g_necon3ad.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon3bd (ph ps : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon3bd_1 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classEq A B).imp ps))) : Nominal.NPrf (ph.imp (ps.neg.imp (Compiler.CompactSourceSyntax.synWne A B)))

Checked nominal proof certificate identified upstream as g_necon3bd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon3d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_necon3d_1 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq C D)))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWne C D).imp (Compiler.CompactSourceSyntax.synWne A B)))

Checked nominal proof certificate identified upstream as g_necon3d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon3i (A B C D : SemanticCore.Class) (hyp_necon3i_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWne C D).imp (Compiler.CompactSourceSyntax.synWne A B))

Checked nominal proof certificate identified upstream as g_necon3i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon3ai (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon3ai_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWne A B).imp ph.neg)

Checked nominal proof certificate identified upstream as g_necon3ai.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon3bi (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon3bi_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp ph)) : Nominal.NPrf (ph.neg.imp (Compiler.CompactSourceSyntax.synWne A B))

Checked nominal proof certificate identified upstream as g_necon3bi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon1ai (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon1ai_1 : Nominal.NPrf (ph.neg.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWne A B).imp ph)

Checked nominal proof certificate identified upstream as g_necon1ai.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon1bi (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon1bi_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWne A B).imp ph)) : Nominal.NPrf (ph.neg.imp (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_necon1bi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon2ai (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon2ai_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp ph.neg)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWne A B))

Checked nominal proof certificate identified upstream as g_necon2ai.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon2bi (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon2bi_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWne A B))) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp ph.neg)

Checked nominal proof certificate identified upstream as g_necon2bi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon2ad (ph ps : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon2ad_1 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classEq A B).imp ps.neg))) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWne A B)))

Checked nominal proof certificate identified upstream as g_necon2ad.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon2bd (ph ps : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon2bd_1 : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWne A B)))) : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classEq A B).imp ps.neg))

Checked nominal proof certificate identified upstream as g_necon2bd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon1bbii (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon1bbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne A B) ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph.neg (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_necon1bbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon2bbii (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necon2bbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWne A B))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A B) ph.neg)

Checked nominal proof certificate identified upstream as g_necon2bbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon4i (A B C D : SemanticCore.Class) (hyp_necon4i_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWne A B).imp (Compiler.CompactSourceSyntax.synWne C D))) : Nominal.NPrf ((SemanticCore.Wff.classEq C D).imp (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_necon4i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecon4d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_necon4d_1 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWne A B).imp (Compiler.CompactSourceSyntax.synWne C D)))) : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classEq C D).imp (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_necon4d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm221ddne (ph ps : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_pm2_21ddne_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_pm2_21ddne_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWne A B))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_pm2_21ddne.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm261ine (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_pm2_61ine_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp ph)) (hyp_pm2_61ine_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWne A B).imp ph)) : Nominal.NPrf ph

Checked nominal proof certificate identified upstream as g_pm2_61ine.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm261dne (ph ps : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_pm2_61dne_1 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classEq A B).imp ps))) (hyp_pm2_61dne_2 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWne A B).imp ps))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_pm2_61dne.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecom (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne A B) (Compiler.CompactSourceSyntax.synWne B A))

Checked nominal proof certificate identified upstream as g_necom.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNecom A B = NFChoice.DirectNominalPrf.WPPReplay.gNecon3bii A B B A (NFChoice.DirectNominalPrf.WPPReplay.gEqcom A B)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecomi (A B : SemanticCore.Class) (hyp_necomi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne B A)

Checked nominal proof certificate identified upstream as g_necomi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecomd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_necomd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWne A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWne B A))

Checked nominal proof certificate identified upstream as g_necomd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNelne2 (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B C).neg).imp (Compiler.CompactSourceSyntax.synWne A B))

Checked nominal proof certificate identified upstream as g_nelne2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalnex (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ph.neg) (Compiler.CompactSourceSyntax.synWrex x A ph).neg)

Checked nominal proof certificate identified upstream as g_ralnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexnal (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph.neg) (Compiler.CompactSourceSyntax.synWral x A ph).neg)

Checked nominal proof certificate identified upstream as g_rexnal.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfral2 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWrex x A ph.neg).neg)

Checked nominal proof certificate identified upstream as g_dfral2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfrex2 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWral x A ph.neg).neg)

Checked nominal proof certificate identified upstream as g_dfrex2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalbida (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralbida_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_ralbida_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ps) (Compiler.CompactSourceSyntax.synWral x A ch)))

Checked nominal proof certificate identified upstream as g_ralbida.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexbida (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralbida_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_ralbida_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ps) (Compiler.CompactSourceSyntax.synWrex x A ch)))

Checked nominal proof certificate identified upstream as g_rexbida.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalbidva (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_ralbidva_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ps) (Compiler.CompactSourceSyntax.synWral x A ch)))

Checked nominal proof certificate identified upstream as g_ralbidva.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexbidva (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_ralbidva_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ps) (Compiler.CompactSourceSyntax.synWrex x A ch)))

Checked nominal proof certificate identified upstream as g_rexbidva.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalbid (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralbid_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_ralbid_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ps) (Compiler.CompactSourceSyntax.synWral x A ch)))

Checked nominal proof certificate identified upstream as g_ralbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexbid (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralbid_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_ralbid_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ps) (Compiler.CompactSourceSyntax.synWrex x A ch)))

Checked nominal proof certificate identified upstream as g_rexbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalbidv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_ralbidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ps) (Compiler.CompactSourceSyntax.synWral x A ch)))

Checked nominal proof certificate identified upstream as g_ralbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexbidv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_ralbidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ps) (Compiler.CompactSourceSyntax.synWrex x A ch)))

Checked nominal proof certificate identified upstream as g_rexbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexbidv2 (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_rexbidv2_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ps) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) ch)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ps) (Compiler.CompactSourceSyntax.synWrex x B ch)))

Checked nominal proof certificate identified upstream as g_rexbidv2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalbii (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWral x A ps))

Checked nominal proof certificate identified upstream as g_ralbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexbii (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex x A ps))

Checked nominal proof certificate identified upstream as g_rexbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2ralbii (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_ralbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ph)) (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ps)))

Checked nominal proof certificate identified upstream as g_n_2ralbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2rexbii (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_ralbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B ph)) (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B ps)))

Checked nominal proof certificate identified upstream as g_n_2rexbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalbii2 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_ralbii2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp ph) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B).imp ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWral x B ps))

Checked nominal proof certificate identified upstream as g_ralbii2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexbii2 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_rexbii2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex x B ps))

Checked nominal proof certificate identified upstream as g_rexbii2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalbiia (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralbiia_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWral x A ps))

Checked nominal proof certificate identified upstream as g_ralbiia.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexbiia (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralbiia_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex x A ps))

Checked nominal proof certificate identified upstream as g_rexbiia.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR2alf (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_x_y : x ≠ y) (hyp_r2alf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y A)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ph)) (SemanticCore.Wff.all x (SemanticCore.Wff.all y ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).imp ph))))

Checked nominal proof certificate identified upstream as g_r2alf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR2exf (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_x_y : x ≠ y) (hyp_r2alf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y A)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B ph)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) ph))))

Checked nominal proof certificate identified upstream as g_r2exf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR2al (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ph)) (SemanticCore.Wff.all x (SemanticCore.Wff.all y ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).imp ph))))

Checked nominal proof certificate identified upstream as g_r2al.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gR2al ph x y A B dv_A_y dv_x_y = NFChoice.DirectNominalPrf.WPPReplay.gR2alf ph x y A B ⋯ (NFChoice.DirectNominalPrf.WPPReplay.gNfcv y A ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR2ex (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B ph)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) ph))))

Checked nominal proof certificate identified upstream as g_r2ex.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gR2ex ph x y A B dv_A_y dv_x_y = NFChoice.DirectNominalPrf.WPPReplay.gR2exf ph x y A B ⋯ (NFChoice.DirectNominalPrf.WPPReplay.gNfcv y A ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2ralbidv (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (hyp_n_2ralbidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ps)) (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ch))))

Checked nominal proof certificate identified upstream as g_n_2ralbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2rexbidv (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (hyp_n_2ralbidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B ps)) (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B ch))))

Checked nominal proof certificate identified upstream as g_n_2rexbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexralbidv (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (hyp_n_2ralbidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWral y B ps)) (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWral y B ch))))

Checked nominal proof certificate identified upstream as g_rexralbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexanali (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWa ph ps.neg)) (Compiler.CompactSourceSyntax.synWral x A (ph.imp ps)).neg)

Checked nominal proof certificate identified upstream as g_rexanali.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRisset (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A B) (Compiler.CompactSourceSyntax.synWrex x B (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)))

Checked nominal proof certificate identified upstream as g_risset.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfra1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWral x A ph))

Checked nominal proof certificate identified upstream as g_nfra1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfrald (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (hyp_nfrald_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_nfrald_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))) (hyp_nfrald_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWral y A ps)))

Checked nominal proof certificate identified upstream as g_nfrald.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfral (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (hyp_nfral_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_nfral_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWral y A ph))

Checked nominal proof certificate identified upstream as g_nfral.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfra2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ph)))

Checked nominal proof certificate identified upstream as g_nfra2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfrex (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (hyp_nfrex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_nfrex_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWrex y A ph))

Checked nominal proof certificate identified upstream as g_nfrex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfre1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWrex x A ph))

Checked nominal proof certificate identified upstream as g_nfre1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexex (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex x A ph).imp (Compiler.CompactSourceSyntax.synWex x ph))

Checked nominal proof certificate identified upstream as g_rexex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRsp (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A ph).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp ph))

Checked nominal proof certificate identified upstream as g_rsp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspe (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph).imp (Compiler.CompactSourceSyntax.synWrex x A ph))

Checked nominal proof certificate identified upstream as g_rspe.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRsp2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ph)).imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).imp ph))

Checked nominal proof certificate identified upstream as g_rsp2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRgen (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_rgen_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x A ph)

Checked nominal proof certificate identified upstream as g_rgen.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRgen2a (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (hyp_rgen2a_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A)).imp ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y A ph))

Checked nominal proof certificate identified upstream as g_rgen2a.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRgenw (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_rgenw_1 : Nominal.NPrf ph) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x A ph)

Checked nominal proof certificate identified upstream as g_rgenw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRgen2w (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_rgenw_1 : Nominal.NPrf ph) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ph))

Checked nominal proof certificate identified upstream as g_rgen2w.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMprg (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_mprg_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A ph).imp ps)) (hyp_mprg_2 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp ph)) : Nominal.NPrf ps

Checked nominal proof certificate identified upstream as g_mprg.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMprg ph ps x A hyp_mprg_1 hyp_mprg_2 = NFChoice.DirectNominalPrf.Nominal.mp (NFChoice.DirectNominalPrf.WPPReplay.gRgen ph x A hyp_mprg_2) hyp_mprg_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMprgbir (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_mprgbir_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWral x A ps))) (hyp_mprgbir_2 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp ps)) : Nominal.NPrf ph

Checked nominal proof certificate identified upstream as g_mprgbir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalim (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A (ph.imp ps)).imp ((Compiler.CompactSourceSyntax.synWral x A ph).imp (Compiler.CompactSourceSyntax.synWral x A ps)))

Checked nominal proof certificate identified upstream as g_ralim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalimi2 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_ralimi2_1 : Nominal.NPrf (((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp ph).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B).imp ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A ph).imp (Compiler.CompactSourceSyntax.synWral x B ps))

Checked nominal proof certificate identified upstream as g_ralimi2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalimia (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralimia_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (ph.imp ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A ph).imp (Compiler.CompactSourceSyntax.synWral x A ps))

Checked nominal proof certificate identified upstream as g_ralimia.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalimiaa (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralimiaa_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph).imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A ph).imp (Compiler.CompactSourceSyntax.synWral x A ps))

Checked nominal proof certificate identified upstream as g_ralimiaa.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalimi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralimi_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A ph).imp (Compiler.CompactSourceSyntax.synWral x A ps))

Checked nominal proof certificate identified upstream as g_ralimi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRal2imi (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ral2imi_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A ph).imp ((Compiler.CompactSourceSyntax.synWral x A ps).imp (Compiler.CompactSourceSyntax.synWral x A ch)))

Checked nominal proof certificate identified upstream as g_ral2imi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalimdaa (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralimdaa_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_ralimdaa_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWral x A ps).imp (Compiler.CompactSourceSyntax.synWral x A ch)))

Checked nominal proof certificate identified upstream as g_ralimdaa.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalimdva (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_ralimdva_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWral x A ps).imp (Compiler.CompactSourceSyntax.synWral x A ch)))

Checked nominal proof certificate identified upstream as g_ralimdva.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalimdv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_ralimdv_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWral x A ps).imp (Compiler.CompactSourceSyntax.synWral x A ch)))

Checked nominal proof certificate identified upstream as g_ralimdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalrimi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralrimi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_ralrimi_2 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWral x A ps))

Checked nominal proof certificate identified upstream as g_ralrimi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalrimiv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_ralrimiv_1 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWral x A ps))

Checked nominal proof certificate identified upstream as g_ralrimiv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalrimiva (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_ralrimiva_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp ps)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWral x A ps))

Checked nominal proof certificate identified upstream as g_ralrimiva.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalrimivw (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_ralrimivw_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWral x A ps))

Checked nominal proof certificate identified upstream as g_ralrimivw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1921t (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWnf x ph).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (ph.imp ps)) (ph.imp (Compiler.CompactSourceSyntax.synWral x A ps))))

Checked nominal proof certificate identified upstream as g_r19_21t.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1921 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_r19_21_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (ph.imp ps)) (ph.imp (Compiler.CompactSourceSyntax.synWral x A ps)))

Checked nominal proof certificate identified upstream as g_r19_21.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gR1921 ph ps x A hyp_r19_21_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_r19_21_1 (NFChoice.DirectNominalPrf.WPPReplay.gR1921t ph ps x A)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1921v (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (ph.imp ps)) (ph.imp (Compiler.CompactSourceSyntax.synWral x A ps)))

Checked nominal proof certificate identified upstream as g_r19_21v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gR1921v ph ps x A dv_ph_x = NFChoice.DirectNominalPrf.WPPReplay.gR1921 ph ps x A (NFChoice.DirectNominalPrf.WPPReplay.gNfv ph x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalrimd (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_ralrimd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_ralrimd_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_ralrimd_3 : Nominal.NPrf (ph.imp (ps.imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp ch)))) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWral x A ch)))

Checked nominal proof certificate identified upstream as g_ralrimd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalrimdv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (hyp_ralrimdv_1 : Nominal.NPrf (ph.imp (ps.imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp ch)))) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWral x A ch)))

Checked nominal proof certificate identified upstream as g_ralrimdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalrimivv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) (hyp_ralrimivv_1 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).imp ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ps)))

Checked nominal proof certificate identified upstream as g_ralrimivv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalrimivva (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) (hyp_ralrimivva_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B))).imp ps)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ps)))

Checked nominal proof certificate identified upstream as g_ralrimivva.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalrimdvv (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_ralrimdvv_1 : Nominal.NPrf (ph.imp (ps.imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).imp ch)))) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ch))))

Checked nominal proof certificate identified upstream as g_ralrimdvv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRgen2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) (hyp_rgen2_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).imp ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ph))

Checked nominal proof certificate identified upstream as g_rgen2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1921bi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_r19_21bi_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWral x A ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp ps)

Checked nominal proof certificate identified upstream as g_r19_21bi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNrex (ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_nrex_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp ps.neg)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWrex x A ps).neg

Checked nominal proof certificate identified upstream as g_nrex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNrexdv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_nrexdv_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp ps.neg)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWrex x A ps).neg)

Checked nominal proof certificate identified upstream as g_nrexdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexim (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x A (ph.imp ps)).imp ((Compiler.CompactSourceSyntax.synWrex x A ph).imp (Compiler.CompactSourceSyntax.synWrex x A ps)))

Checked nominal proof certificate identified upstream as g_rexim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReximia (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_reximia_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (ph.imp ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex x A ph).imp (Compiler.CompactSourceSyntax.synWrex x A ps))

Checked nominal proof certificate identified upstream as g_reximia.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReximi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_reximi_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex x A ph).imp (Compiler.CompactSourceSyntax.synWrex x A ps))

Checked nominal proof certificate identified upstream as g_reximi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReximdai (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_reximdai_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_reximdai_2 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (ps.imp ch)))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWrex x A ps).imp (Compiler.CompactSourceSyntax.synWrex x A ch)))

Checked nominal proof certificate identified upstream as g_reximdai.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReximdvai (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_reximdvai_1 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (ps.imp ch)))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWrex x A ps).imp (Compiler.CompactSourceSyntax.synWrex x A ch)))

Checked nominal proof certificate identified upstream as g_reximdvai.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReximdv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_reximdv_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWrex x A ps).imp (Compiler.CompactSourceSyntax.synWrex x A ch)))

Checked nominal proof certificate identified upstream as g_reximdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReximdva (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_reximdva_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWrex x A ps).imp (Compiler.CompactSourceSyntax.synWrex x A ch)))

Checked nominal proof certificate identified upstream as g_reximdva.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1923t (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWnf x ps).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (ph.imp ps)) ((Compiler.CompactSourceSyntax.synWrex x A ph).imp ps)))

Checked nominal proof certificate identified upstream as g_r19_23t.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1923 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_r19_23_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (ph.imp ps)) ((Compiler.CompactSourceSyntax.synWrex x A ph).imp ps))

Checked nominal proof certificate identified upstream as g_r19_23.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gR1923 ph ps x A hyp_r19_23_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_r19_23_1 (NFChoice.DirectNominalPrf.WPPReplay.gR1923t ph ps x A)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1923v (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ps_x : x ∉ ps.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (ph.imp ps)) ((Compiler.CompactSourceSyntax.synWrex x A ph).imp ps))

Checked nominal proof certificate identified upstream as g_r19_23v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gR1923v ph ps x A dv_ps_x = NFChoice.DirectNominalPrf.WPPReplay.gR1923 ph ps x A (NFChoice.DirectNominalPrf.WPPReplay.gNfv ps x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_rexlimi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_rexlimi_2 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (ph.imp ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex x A ph).imp ps)

Checked nominal proof certificate identified upstream as g_rexlimi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimiv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ps_x : x ∉ ps.fv) (hyp_rexlimiv_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (ph.imp ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex x A ph).imp ps)

Checked nominal proof certificate identified upstream as g_rexlimiv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimiva (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ps_x : x ∉ ps.fv) (hyp_rexlimiva_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph).imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex x A ph).imp ps)

Checked nominal proof certificate identified upstream as g_rexlimiva.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimivw (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ps_x : x ∉ ps.fv) (hyp_rexlimivw_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex x A ph).imp ps)

Checked nominal proof certificate identified upstream as g_rexlimivw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimd (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_rexlimd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_rexlimd_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ch)) (hyp_rexlimd_3 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (ps.imp ch)))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWrex x A ps).imp ch))

Checked nominal proof certificate identified upstream as g_rexlimd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimdv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_rexlimdv_1 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (ps.imp ch)))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWrex x A ps).imp ch))

Checked nominal proof certificate identified upstream as g_rexlimdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimdva (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_rexlimdva_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWrex x A ps).imp ch))

Checked nominal proof certificate identified upstream as g_rexlimdva.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimdvaa (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_rexlimdvaa_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ps)).imp ch)) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWrex x A ps).imp ch))

Checked nominal proof certificate identified upstream as g_rexlimdvaa.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimdv3a (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_rexlimdv3a_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ps).imp ch)) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWrex x A ps).imp ch))

Checked nominal proof certificate identified upstream as g_rexlimdv3a.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimdvw (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_rexlimdvw_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWrex x A ps).imp ch))

Checked nominal proof certificate identified upstream as g_rexlimdvw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimddv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_rexlimddv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWrex x A ps))) (hyp_rexlimddv_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ps)).imp ch)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_rexlimddv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimivv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_rexlimivv_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).imp (ph.imp ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B ph)).imp ps)

Checked nominal proof certificate identified upstream as g_rexlimivv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimdvv (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_ch_x : x ∉ ch.fv) (dv_ch_y : y ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) (hyp_rexlimdvv_1 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)).imp (ps.imp ch)))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B ps)).imp ch))

Checked nominal proof certificate identified upstream as g_rexlimdvv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexlimdvva (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_ch_x : x ∉ ch.fv) (dv_ch_y : y ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) (hyp_rexlimdvva_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B))).imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B ps)).imp ch))

Checked nominal proof certificate identified upstream as g_rexlimdvva.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1926 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWral x A ps)))

Checked nominal proof certificate identified upstream as g_r19_26.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.g_r19_26_2 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B (Compiler.CompactSourceSyntax.synWa ph ps))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ph)) (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ps))))

Checked nominal proof certificate identified upstream as g_r19_26_2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalbiim (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWb ph ps)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWral x A (ph.imp ps)) (Compiler.CompactSourceSyntax.synWral x A (ps.imp ph))))

Checked nominal proof certificate identified upstream as g_ralbiim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1927av (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ps_x : x ∉ ps.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWral x A ph) ps).imp (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_r19_27av.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1928av (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWral x A ps)).imp (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_r19_28av.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1929 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWrex x A ps)).imp (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_r19_29.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1935 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (ph.imp ps)) ((Compiler.CompactSourceSyntax.synWral x A ph).imp (Compiler.CompactSourceSyntax.synWrex x A ps)))

Checked nominal proof certificate identified upstream as g_r19_35.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1941 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_r19_41_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWrex x A ph) ps))

Checked nominal proof certificate identified upstream as g_r19_41.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1941v (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ps_x : x ∉ ps.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWrex x A ph) ps))

Checked nominal proof certificate identified upstream as g_r19_41v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gR1941v ph ps x A dv_ps_x = NFChoice.DirectNominalPrf.WPPReplay.gR1941 ph ps x A (NFChoice.DirectNominalPrf.WPPReplay.gNfv ps x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1942v (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWrex x A ps)))

Checked nominal proof certificate identified upstream as g_r19_42v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR1943 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWo ph ps)) (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex x A ps)))

Checked nominal proof certificate identified upstream as g_r19_43.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalcomf (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_x_y : x ≠ y) (hyp_ralcomf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y A)) (hyp_ralcomf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ph)) (Compiler.CompactSourceSyntax.synWral y B (Compiler.CompactSourceSyntax.synWral x A ph)))

Checked nominal proof certificate identified upstream as g_ralcomf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexcomf (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_x_y : x ≠ y) (hyp_ralcomf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y A)) (hyp_ralcomf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B ph)) (Compiler.CompactSourceSyntax.synWrex y B (Compiler.CompactSourceSyntax.synWrex x A ph)))

Checked nominal proof certificate identified upstream as g_rexcomf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalcom (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ph)) (Compiler.CompactSourceSyntax.synWral y B (Compiler.CompactSourceSyntax.synWral x A ph)))

Checked nominal proof certificate identified upstream as g_ralcom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexcom (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B ph)) (Compiler.CompactSourceSyntax.synWrex y B (Compiler.CompactSourceSyntax.synWrex x A ph)))

Checked nominal proof certificate identified upstream as g_rexcom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReean (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_x_y : x ≠ y) (hyp_reean_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_reean_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B (Compiler.CompactSourceSyntax.synWa ph ps))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex y B ps)))

Checked nominal proof certificate identified upstream as g_reean.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReeanv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWrex y B (Compiler.CompactSourceSyntax.synWa ph ps))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex y B ps)))

Checked nominal proof certificate identified upstream as g_reeanv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRabid2 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCrab x A ph)) (Compiler.CompactSourceSyntax.synWral x A ph))

Checked nominal proof certificate identified upstream as g_rabid2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRabbi (ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWb ps ch)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrab x A ps) (Compiler.CompactSourceSyntax.synCrab x A ch)))

Checked nominal proof certificate identified upstream as g_rabbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRaleqf (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_raleq1f_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_raleq1f_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWral x B ph)))

Checked nominal proof certificate identified upstream as g_raleqf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexeqf (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_raleq1f_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_raleq1f_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex x B ph)))

Checked nominal proof certificate identified upstream as g_rexeqf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRaleq (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWral x B ph)))

Checked nominal proof certificate identified upstream as g_raleq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexeq (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex x B ph)))

Checked nominal proof certificate identified upstream as g_rexeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRaleqi (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_raleq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWral x B ph))

Checked nominal proof certificate identified upstream as g_raleqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gRaleqi ph x A B dv_A_x dv_B_x hyp_raleq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_raleq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gRaleq ph x A B ⋯ ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexeqi (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_raleq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex x B ph))

Checked nominal proof certificate identified upstream as g_rexeqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gRexeqi ph x A B dv_A_x dv_B_x hyp_raleq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_raleq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gRexeq ph x A B ⋯ ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRaleqdv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_raleq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ps) (Compiler.CompactSourceSyntax.synWral x B ps)))

Checked nominal proof certificate identified upstream as g_raleqdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexeqdv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_raleq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ps) (Compiler.CompactSourceSyntax.synWrex x B ps)))

Checked nominal proof certificate identified upstream as g_rexeqdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRaleqbi1dv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_raleqd_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWral x B ps)))

Checked nominal proof certificate identified upstream as g_raleqbi1dv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexeqbi1dv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_raleqd_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex x B ps)))

Checked nominal proof certificate identified upstream as g_rexeqbi1dv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRaleqbidv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ph_x : x ∉ ph.fv) (hyp_raleqbidv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_raleqbidv_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ps) (Compiler.CompactSourceSyntax.synWral x B ch)))

Checked nominal proof certificate identified upstream as g_raleqbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexeqbidv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ph_x : x ∉ ph.fv) (hyp_raleqbidv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_raleqbidv_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ps) (Compiler.CompactSourceSyntax.synWrex x B ch)))

Checked nominal proof certificate identified upstream as g_rexeqbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReu5 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWreu x A ph) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrmo x A ph)))

Checked nominal proof certificate identified upstream as g_reu5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvralf (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (hyp_cbvralf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_cbvralf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y A)) (hyp_cbvralf_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_cbvralf_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbvralf_5 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWral y A ps))

Checked nominal proof certificate identified upstream as g_cbvralf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvrexf (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (hyp_cbvralf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_cbvralf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y A)) (hyp_cbvralf_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_cbvralf_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbvralf_5 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex y A ps))

Checked nominal proof certificate identified upstream as g_cbvrexf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvral (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (hyp_cbvral_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_cbvral_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbvral_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWral y A ps))

Checked nominal proof certificate identified upstream as g_cbvral.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvrex (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (hyp_cbvral_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_cbvral_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbvral_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex y A ps))

Checked nominal proof certificate identified upstream as g_cbvrex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvralv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (hyp_cbvralv_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A ph) (Compiler.CompactSourceSyntax.synWral y A ps))

Checked nominal proof certificate identified upstream as g_cbvralv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvrexv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (hyp_cbvralv_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex y A ps))

Checked nominal proof certificate identified upstream as g_cbvrexv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvral2v (ph ps ch : SemanticCore.Wff) (x y z w : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_w : w ∉ B.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_ch_w : w ∉ ch.fv) (dv_ch_x : x ∉ ch.fv) (dv_ph_z : z ∉ ph.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (dv_y_z : y ≠ z) (hyp_cbvral2v_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x z).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_cbvral2v_2 : Nominal.NPrf ((SemanticCore.Wff.objEq y w).imp (Compiler.CompactSourceSyntax.synWb ch ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y B ph)) (Compiler.CompactSourceSyntax.synWral z A (Compiler.CompactSourceSyntax.synWral w B ps)))

Checked nominal proof certificate identified upstream as g_cbvral2v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvrexsv (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_ph_y : y ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWrex y A (Compiler.CompactSourceSyntax.synWsb y x ph)))

Checked nominal proof certificate identified upstream as g_cbvrexsv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRabbidva (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_rabbidva_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrab x A ps) (Compiler.CompactSourceSyntax.synCrab x A ch)))

Checked nominal proof certificate identified upstream as g_rabbidva.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRabbidv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_rabbidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrab x A ps) (Compiler.CompactSourceSyntax.synCrab x A ch)))

Checked nominal proof certificate identified upstream as g_rabbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRabeqf (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_rabeqf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_rabeqf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrab x A ph) (Compiler.CompactSourceSyntax.synCrab x B ph)))

Checked nominal proof certificate identified upstream as g_rabeqf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRabeq (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrab x A ph) (Compiler.CompactSourceSyntax.synCrab x B ph)))

Checked nominal proof certificate identified upstream as g_rabeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVex (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_vex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsset (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)))

Checked nominal proof certificate identified upstream as g_isset.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIssetf (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_issetf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)))

Checked nominal proof certificate identified upstream as g_issetf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsseti (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_isseti_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A))

Checked nominal proof certificate identified upstream as g_isseti.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElex (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A B).imp (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_elex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElexi (A B : SemanticCore.Class) (hyp_elisseti_1 : Nominal.NPrf (SemanticCore.Wff.classMem A B)) : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_elexi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gElexi A B hyp_elisseti_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_elisseti_1 (NFChoice.DirectNominalPrf.WPPReplay.gElex A B)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElisset (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)))

Checked nominal proof certificate identified upstream as g_elisset.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalv (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x Compiler.CompactSourceSyntax.synCvv ph) (SemanticCore.Wff.all x ph))

Checked nominal proof certificate identified upstream as g_ralv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexv (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x Compiler.CompactSourceSyntax.synCvv ph) (Compiler.CompactSourceSyntax.synWex x ph))

Checked nominal proof certificate identified upstream as g_rexv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRabab (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrab x Compiler.CompactSourceSyntax.synCvv ph) (SemanticCore.Class.cab x ph))

Checked nominal proof certificate identified upstream as g_rabab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalcom4 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (SemanticCore.Wff.all y ph)) (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWral x A ph)))

Checked nominal proof certificate identified upstream as g_ralcom4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexcom4 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWex y ph)) (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWrex x A ph)))

Checked nominal proof certificate identified upstream as g_rexcom4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCeqsalg (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_ceqsalg_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_ceqsalg_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp ph)) ps))

Checked nominal proof certificate identified upstream as g_ceqsalg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCeqsal (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_ceqsal_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_ceqsal_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_ceqsal_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp ph)) ps)

Checked nominal proof certificate identified upstream as g_ceqsal.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCeqsalv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_ceqsalv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_ceqsalv_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp ph)) ps)

Checked nominal proof certificate identified upstream as g_ceqsalv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCeqsex (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_ceqsex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_ceqsex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_ceqsex_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) ph)) ps)

Checked nominal proof certificate identified upstream as g_ceqsex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCeqsexv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_ceqsexv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_ceqsexv_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) ph)) ps)

Checked nominal proof certificate identified upstream as g_ceqsexv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCeqsex2 (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) (hyp_ceqsex2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_ceqsex2_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ch)) (hyp_ceqsex2_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_ceqsex2_4 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_ceqsex2_5 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_ceqsex2_6 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B) ph))) ch)

Checked nominal proof certificate identified upstream as g_ceqsex2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCeqsex2v (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ch_y : y ∉ ch.fv) (dv_ps_x : x ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_ceqsex2v_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_ceqsex2v_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_ceqsex2v_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_ceqsex2v_4 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B) ph))) ch)

Checked nominal proof certificate identified upstream as g_ceqsex2v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtoclgft (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWnfc x A) (Compiler.CompactSourceSyntax.synWnf x ps)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.all x ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (SemanticCore.Wff.all x ph)) (SemanticCore.Wff.classMem A V)).imp ps)

Checked nominal proof certificate identified upstream as g_vtoclgft.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtocldf (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (hyp_vtocld_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A V))) (hyp_vtocld_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_vtocld_3 : Nominal.NPrf (ph.imp ps)) (hyp_vtocldf_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_vtocldf_5 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))) (hyp_vtocldf_6 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ch))) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_vtocldf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtocld (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_vtocld_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A V))) (hyp_vtocld_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_vtocld_3 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_vtocld.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtoclf (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_vtoclf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_vtoclf_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_vtoclf_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_vtoclf_4 : Nominal.NPrf ph) : Nominal.NPrf ps

Checked nominal proof certificate identified upstream as g_vtoclf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtocl (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_vtocl_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_vtocl_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_vtocl_3 : Nominal.NPrf ph) : Nominal.NPrf ps

Checked nominal proof certificate identified upstream as g_vtocl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtocl2 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_vtocl2_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_vtocl2_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_vtocl2_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_vtocl2_4 : Nominal.NPrf ph) : Nominal.NPrf ps

Checked nominal proof certificate identified upstream as g_vtocl2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtoclb (ph ps ch th : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ch_x : x ∉ ch.fv) (dv_th_x : x ∉ th.fv) (hyp_vtoclb_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_vtoclb_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_vtoclb_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ps th))) (hyp_vtoclb_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)

Checked nominal proof certificate identified upstream as g_vtoclb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtoclgf (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (hyp_vtoclgf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_vtoclgf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_vtoclgf_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_vtoclgf_4 : Nominal.NPrf ph) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp ps)

Checked nominal proof certificate identified upstream as g_vtoclgf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtoclg (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_vtoclg_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_vtoclg_2 : Nominal.NPrf ph) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp ps)

Checked nominal proof certificate identified upstream as g_vtoclg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtoclbg (ph ps ch th : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ch_x : x ∉ ch.fv) (dv_th_x : x ∉ th.fv) (hyp_vtoclbg_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_vtoclbg_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ps th))) (hyp_vtoclbg_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb ch th))

Checked nominal proof certificate identified upstream as g_vtoclbg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtocl2gf (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B V W : SemanticCore.Class) (hyp_vtocl2gf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_vtocl2gf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y A)) (hyp_vtocl2gf_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y B)) (hyp_vtocl2gf_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_vtocl2gf_5 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ch)) (hyp_vtocl2gf_6 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_vtocl2gf_7 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_vtocl2gf_8 : Nominal.NPrf ph) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp ch)

Checked nominal proof certificate identified upstream as g_vtocl2gf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtocl2g (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_ch_y : y ∉ ch.fv) (dv_ps_x : x ∉ ps.fv) (hyp_vtocl2g_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_vtocl2g_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_vtocl2g_3 : Nominal.NPrf ph) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp ch)

Checked nominal proof certificate identified upstream as g_vtocl2g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtoclgaf (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_B_x : x ∉ B.fv) (hyp_vtoclgaf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_vtoclgaf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_vtoclgaf_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_vtoclgaf_4 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B).imp ph)) : Nominal.NPrf ((SemanticCore.Wff.classMem A B).imp ps)

Checked nominal proof certificate identified upstream as g_vtoclgaf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtoclga (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (hyp_vtoclga_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_vtoclga_2 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B).imp ph)) : Nominal.NPrf ((SemanticCore.Wff.classMem A B).imp ps)

Checked nominal proof certificate identified upstream as g_vtoclga.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtocl2gaf (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B C D : SemanticCore.Class) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_x_y : x ≠ y) (hyp_vtocl2gaf_a : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_vtocl2gaf_b : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y A)) (hyp_vtocl2gaf_c : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y B)) (hyp_vtocl2gaf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_vtocl2gaf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ch)) (hyp_vtocl2gaf_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_vtocl2gaf_4 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_vtocl2gaf_5 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D)).imp ph)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)).imp ch)

Checked nominal proof certificate identified upstream as g_vtocl2gaf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtocl2ga (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B C D : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_ch_y : y ∉ ch.fv) (dv_ps_x : x ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_vtocl2ga_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_vtocl2ga_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_vtocl2ga_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D)).imp ph)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)).imp ch)

Checked nominal proof certificate identified upstream as g_vtocl2ga.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVtocleg (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ph_x : x ∉ ph.fv) (hyp_vtocleg_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp ph)) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp ph)

Checked nominal proof certificate identified upstream as g_vtocleg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpcimgft (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_spcimgft_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_spcimgft_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) : Nominal.NPrf ((SemanticCore.Wff.all x ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (ph.imp ps))).imp ((SemanticCore.Wff.classMem A B).imp ((SemanticCore.Wff.all x ph).imp ps)))

Checked nominal proof certificate identified upstream as g_spcimgft.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpcgft (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_spcimgft_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_spcimgft_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) : Nominal.NPrf ((SemanticCore.Wff.all x ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))).imp ((SemanticCore.Wff.classMem A B).imp ((SemanticCore.Wff.all x ph).imp ps)))

Checked nominal proof certificate identified upstream as g_spcgft.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpcgf (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (hyp_spcgf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_spcgf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_spcgf_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp ((SemanticCore.Wff.all x ph).imp ps))

Checked nominal proof certificate identified upstream as g_spcgf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpcegf (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (hyp_spcgf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_spcgf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_spcgf_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (ps.imp (Compiler.CompactSourceSyntax.synWex x ph)))

Checked nominal proof certificate identified upstream as g_spcegf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpcimdv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_spcimdv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A B))) (hyp_spcimdv_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)).imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((SemanticCore.Wff.all x ps).imp ch))

Checked nominal proof certificate identified upstream as g_spcimdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpcimedv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_spcimdv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A B))) (hyp_spcimedv_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)).imp (ch.imp ps))) : Nominal.NPrf (ph.imp (ch.imp (Compiler.CompactSourceSyntax.synWex x ps)))

Checked nominal proof certificate identified upstream as g_spcimedv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpcgv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_spcgv_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp ((SemanticCore.Wff.all x ph).imp ps))

Checked nominal proof certificate identified upstream as g_spcgv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpcegv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_spcgv_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (ps.imp (Compiler.CompactSourceSyntax.synWex x ph)))

Checked nominal proof certificate identified upstream as g_spcegv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpc2egv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_spc2egv_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (ps.imp (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ph))))

Checked nominal proof certificate identified upstream as g_spc2egv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpc2gv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_spc2egv_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp ((SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)).imp ps))

Checked nominal proof certificate identified upstream as g_spc2gv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpc3egv (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B C V W X : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_ps_z : z ∉ ps.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_spc3egv_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B) (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) C)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W) (SemanticCore.Wff.classMem C X)).imp (ps.imp (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWex z ph)))))

Checked nominal proof certificate identified upstream as g_spc3egv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpc3gv (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B C V W X : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_ps_z : z ∉ ps.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_spc3egv_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B) (SemanticCore.Wff.classEq (SemanticCore.Class.cv z) C)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W) (SemanticCore.Wff.classMem C X)).imp ((SemanticCore.Wff.all x (SemanticCore.Wff.all y (SemanticCore.Wff.all z ph))).imp ps))

Checked nominal proof certificate identified upstream as g_spc3gv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpcv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_spcv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_spcv_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ps)

Checked nominal proof certificate identified upstream as g_spcv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpcev (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_spcv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_spcv_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (ps.imp (Compiler.CompactSourceSyntax.synWex x ph))

Checked nominal proof certificate identified upstream as g_spcev.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpc2ev (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_spc2ev_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_spc2ev_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_spc2ev_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (ps.imp (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ph)))

Checked nominal proof certificate identified upstream as g_spc2ev.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspc (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_rspc_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_rspc_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.classMem A B).imp ((Compiler.CompactSourceSyntax.synWral x B ph).imp ps))

Checked nominal proof certificate identified upstream as g_rspc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspce (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_rspc_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_rspc_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A B) ps).imp (Compiler.CompactSourceSyntax.synWrex x B ph))

Checked nominal proof certificate identified upstream as g_rspce.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspcv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (hyp_rspcv_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.classMem A B).imp ((Compiler.CompactSourceSyntax.synWral x B ph).imp ps))

Checked nominal proof certificate identified upstream as g_rspcv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspccv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (hyp_rspcv_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral x B ph).imp ((SemanticCore.Wff.classMem A B).imp ps))

Checked nominal proof certificate identified upstream as g_rspccv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspcva (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (hyp_rspcv_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A B) (Compiler.CompactSourceSyntax.synWral x B ph)).imp ps)

Checked nominal proof certificate identified upstream as g_rspcva.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspccva (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (hyp_rspcv_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWral x B ph) (SemanticCore.Wff.classMem A B)).imp ps)

Checked nominal proof certificate identified upstream as g_rspccva.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspcev (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ps_x : x ∉ ps.fv) (hyp_rspcv_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A B) ps).imp (Compiler.CompactSourceSyntax.synWrex x B ph))

Checked nominal proof certificate identified upstream as g_rspcev.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspcimdv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_rspcimdv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A B))) (hyp_rspcimdv_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)).imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWral x B ps).imp ch))

Checked nominal proof certificate identified upstream as g_rspcimdv.

Equations

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