NF weak partition development: NominalWPPReplayChunk005.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbae (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (SemanticCore.Wff.all z (SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y))))

Checked nominal proof certificate identified upstream as g_hbae.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfae (x y z : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z (SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)))

Checked nominal proof certificate identified upstream as g_nfae.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfnae (x y z : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z (SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg)

Checked nominal proof certificate identified upstream as g_nfnae.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfeqf (x y z : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.all z (SemanticCore.Wff.objEq z x)).neg (SemanticCore.Wff.all z (SemanticCore.Wff.objEq z y)).neg).imp (Compiler.CompactSourceSyntax.synWnf z (SemanticCore.Wff.objEq x y)))

Checked nominal proof certificate identified upstream as g_nfeqf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqus4 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph)).imp (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x y) ph)))

Checked nominal proof certificate identified upstream as g_equs4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqusal (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_equsal_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_equsal_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph)) ps)

Checked nominal proof certificate identified upstream as g_equsal.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqusex (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_equsex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_equsex_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x y) ph)) ps)

Checked nominal proof certificate identified upstream as g_equsex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDral1 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_dral1_1 : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ph) (SemanticCore.Wff.all y ps)))

Checked nominal proof certificate identified upstream as g_dral1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDral2 (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (hyp_dral1_1 : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all z ph) (SemanticCore.Wff.all z ps)))

Checked nominal proof certificate identified upstream as g_dral2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDrex1 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_dral1_1 : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWex y ps)))

Checked nominal proof certificate identified upstream as g_drex1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDrnf1 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_dral1_1 : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWnf x ph) (Compiler.CompactSourceSyntax.synWnf y ps)))

Checked nominal proof certificate identified upstream as g_drnf1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDrnf2 (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (hyp_dral1_1 : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWnf z ph) (Compiler.CompactSourceSyntax.synWnf z ps)))

Checked nominal proof certificate identified upstream as g_drnf2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfald2 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfald2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_nfald2_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.synWnf x (SemanticCore.Wff.all y ps)))

Checked nominal proof certificate identified upstream as g_nfald2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfexd2 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfald2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_nfald2_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.synWnf x (Compiler.CompactSourceSyntax.synWex y ps)))

Checked nominal proof certificate identified upstream as g_nfexd2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpimt (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWnf x ps) (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp (ph.imp ps)))).imp ((SemanticCore.Wff.all x ph).imp ps))

Checked nominal proof certificate identified upstream as g_spimt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpim (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_spim_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_spim_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp ps))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ps)

Checked nominal proof certificate identified upstream as g_spim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpime (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_spime_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_spime_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWex x ps))

Checked nominal proof certificate identified upstream as g_spime.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpimed (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_spimed_1 : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWnf x ph))) (hyp_spimed_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp ps))) : Nominal.NPrf (ch.imp (ph.imp (Compiler.CompactSourceSyntax.synWex x ps)))

Checked nominal proof certificate identified upstream as g_spimed.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbv1h (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_cbv1h_1 : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all y ps)))) (hyp_cbv1h_2 : Nominal.NPrf (ph.imp (ch.imp (SemanticCore.Wff.all x ch)))) (hyp_cbv1h_3 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.objEq x y).imp (ps.imp ch)))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)).imp ((SemanticCore.Wff.all x ps).imp (SemanticCore.Wff.all y ch)))

Checked nominal proof certificate identified upstream as g_cbv1h.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbv1 (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_cbv1_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf y ps))) (hyp_cbv1_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ch))) (hyp_cbv1_3 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.objEq x y).imp (ps.imp ch)))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)).imp ((SemanticCore.Wff.all x ps).imp (SemanticCore.Wff.all y ch)))

Checked nominal proof certificate identified upstream as g_cbv1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbv2h (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_cbv2h_1 : Nominal.NPrf (ph.imp (ps.imp (SemanticCore.Wff.all y ps)))) (hyp_cbv2h_2 : Nominal.NPrf (ph.imp (ch.imp (SemanticCore.Wff.all x ch)))) (hyp_cbv2h_3 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ps ch)))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ps) (SemanticCore.Wff.all y ch)))

Checked nominal proof certificate identified upstream as g_cbv2h.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbv2 (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_cbv2_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf y ps))) (hyp_cbv2_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ch))) (hyp_cbv2_3 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ps ch)))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ps) (SemanticCore.Wff.all y ch)))

Checked nominal proof certificate identified upstream as g_cbv2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbv3 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_cbv3_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_cbv3_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbv3_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp ps))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp (SemanticCore.Wff.all y ps))

Checked nominal proof certificate identified upstream as g_cbv3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbv3h (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_cbv3h_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all y ph))) (hyp_cbv3h_2 : Nominal.NPrf (ps.imp (SemanticCore.Wff.all x ps))) (hyp_cbv3h_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp ps))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp (SemanticCore.Wff.all y ps))

Checked nominal proof certificate identified upstream as g_cbv3h.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbval (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_cbval_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_cbval_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbval_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ph) (SemanticCore.Wff.all y ps))

Checked nominal proof certificate identified upstream as g_cbval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvex (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_cbvex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_cbvex_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbvex_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWex y ps))

Checked nominal proof certificate identified upstream as g_cbvex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gChvar (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_chvar_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_chvar_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_chvar_3 : Nominal.NPrf ph) : Nominal.NPrf ps

Checked nominal proof certificate identified upstream as g_chvar.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEquvini (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x z) (SemanticCore.Wff.objEq z y))))

Checked nominal proof certificate identified upstream as g_equvini.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpimv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) (hyp_spimv_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp ps))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ps)

Checked nominal proof certificate identified upstream as g_spimv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSpimv ph ps x y dv_ps_x hyp_spimv_1 = NFChoice.DirectNominalPrf.WPPReplay.gSpim ph ps x y (NFChoice.DirectNominalPrf.WPPReplay.gNfv ps x ⋯) hyp_spimv_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx11v2 (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_ph_z : z ∉ ph.fv) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_ax11v2_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x z).imp (ph.imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x z).imp ph))))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp ((SemanticCore.Wff.objEq x y).imp (ph.imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph)))))

Checked nominal proof certificate identified upstream as g_ax11v2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx11a2 (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_ph_z : z ∉ ph.fv) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_ax11a2_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x z).imp ((SemanticCore.Wff.all z ph).imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x z).imp ph))))) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp ((SemanticCore.Wff.objEq x y).imp (ph.imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph)))))

Checked nominal proof certificate identified upstream as g_ax11a2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx11o (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp ((SemanticCore.Wff.objEq x y).imp (ph.imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph)))))

Checked nominal proof certificate identified upstream as g_ax11o.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqus5 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp ((Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x y) ph)).imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph))))

Checked nominal proof certificate identified upstream as g_equs5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ps_x : x ∉ ps.fv) (hyp_spv_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp ps)

Checked nominal proof certificate identified upstream as g_spv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvalv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (hyp_cbvalv_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ph) (SemanticCore.Wff.all y ps))

Checked nominal proof certificate identified upstream as g_cbvalv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvexv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (hyp_cbvalv_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWex y ps))

Checked nominal proof certificate identified upstream as g_cbvexv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbval2 (ph ps : SemanticCore.Wff) (x y z w : SemanticCore.Var) (dv_w_x : w ≠ x) (dv_w_z : w ≠ z) (dv_x_y : x ≠ y) (dv_y_z : y ≠ z) (hyp_cbval2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z ph)) (hyp_cbval2_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf w ph)) (hyp_cbval2_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbval2_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ps)) (hyp_cbval2_5 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x z) (SemanticCore.Wff.objEq y w)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)) (SemanticCore.Wff.all z (SemanticCore.Wff.all w ps)))

Checked nominal proof certificate identified upstream as g_cbval2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvex2 (ph ps : SemanticCore.Wff) (x y z w : SemanticCore.Var) (dv_w_x : w ≠ x) (dv_w_z : w ≠ z) (dv_x_y : x ≠ y) (dv_y_z : y ≠ z) (hyp_cbval2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z ph)) (hyp_cbval2_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf w ph)) (hyp_cbval2_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbval2_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ps)) (hyp_cbval2_5 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x z) (SemanticCore.Wff.objEq y w)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y ph)) (Compiler.CompactSourceSyntax.synWex z (Compiler.CompactSourceSyntax.synWex w ps)))

Checked nominal proof certificate identified upstream as g_cbvex2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbval2v (ph ps : SemanticCore.Wff) (x y z w : SemanticCore.Var) (dv_ph_w : w ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_w_x : w ≠ x) (dv_w_z : w ≠ z) (dv_x_y : x ≠ y) (dv_y_z : y ≠ z) (hyp_cbval2v_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x z) (SemanticCore.Wff.objEq y w)).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x (SemanticCore.Wff.all y ph)) (SemanticCore.Wff.all z (SemanticCore.Wff.all w ps)))

Checked nominal proof certificate identified upstream as g_cbval2v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvald (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_cbvald_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_cbvald_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf y ps))) (hyp_cbvald_3 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ps ch)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ps) (SemanticCore.Wff.all y ch)))

Checked nominal proof certificate identified upstream as g_cbvald.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvexd (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_cbvald_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_cbvald_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf y ps))) (hyp_cbvald_3 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ps ch)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x ps) (Compiler.CompactSourceSyntax.synWex y ch)))

Checked nominal proof certificate identified upstream as g_cbvexd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDrsb1 (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb z x ph) (Compiler.CompactSourceSyntax.synWsb z y ph)))

Checked nominal proof certificate identified upstream as g_drsb1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSb2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph)).imp (Compiler.CompactSourceSyntax.synWsb y x ph))

Checked nominal proof certificate identified upstream as g_sb2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gStdpc4 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x ph).imp (Compiler.CompactSourceSyntax.synWsb y x ph))

Checked nominal proof certificate identified upstream as g_stdpc4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbft (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWnf x ph).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ph) ph))

Checked nominal proof certificate identified upstream as g_sbft.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbf (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_sbf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ph) ph)

Checked nominal proof certificate identified upstream as g_sbf.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSbf ph x y hyp_sbf_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_sbf_1 (NFChoice.DirectNominalPrf.WPPReplay.gSbft ph x y)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqusb2 (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWsb y x (SemanticCore.Wff.objEq y x))

Checked nominal proof certificate identified upstream as g_equsb2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbied (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_sbied_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_sbied_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ch))) (hyp_sbied_3 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ps ch)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ps) ch))

Checked nominal proof certificate identified upstream as g_sbied.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbie (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_sbie_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_sbie_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ph) ps)

Checked nominal proof certificate identified upstream as g_sbie.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbsb2a (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWsb y x (SemanticCore.Wff.all y ph)).imp (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWsb y x ph)))

Checked nominal proof certificate identified upstream as g_hbsb2a.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbsb3 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_hbsb3_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all y ph))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWsb y x ph).imp (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWsb y x ph)))

Checked nominal proof certificate identified upstream as g_hbsb3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfs1 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfs1_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWsb y x ph))

Checked nominal proof certificate identified upstream as g_nfs1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx16 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (ph.imp (SemanticCore.Wff.all x ph)))

Checked nominal proof certificate identified upstream as g_ax16.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAx16 ph x y dv_x_y = NFChoice.DirectNominalPrf.WPPReplay.gA16g ph x y x ⋯

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA16nf (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).imp (Compiler.CompactSourceSyntax.synWnf z ph))

Checked nominal proof certificate identified upstream as g_a16nf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSb4 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp ((Compiler.CompactSourceSyntax.synWsb y x ph).imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph))))

Checked nominal proof certificate identified upstream as g_sb4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSb4b (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ph) (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph))))

Checked nominal proof certificate identified upstream as g_sb4b.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbsb2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp ((Compiler.CompactSourceSyntax.synWsb y x ph).imp (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWsb y x ph))))

Checked nominal proof certificate identified upstream as g_hbsb2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfsb2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWsb y x ph)))

Checked nominal proof certificate identified upstream as g_nfsb2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbequi (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp ((Compiler.CompactSourceSyntax.synWsb x z ph).imp (Compiler.CompactSourceSyntax.synWsb y z ph)))

Checked nominal proof certificate identified upstream as g_sbequi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbequ (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb x z ph) (Compiler.CompactSourceSyntax.synWsb y z ph)))

Checked nominal proof certificate identified upstream as g_sbequ.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbn (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ph.neg) (Compiler.CompactSourceSyntax.synWsb y x ph).neg)

Checked nominal proof certificate identified upstream as g_sbn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbi1 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWsb y x (ph.imp ps)).imp ((Compiler.CompactSourceSyntax.synWsb y x ph).imp (Compiler.CompactSourceSyntax.synWsb y x ps)))

Checked nominal proof certificate identified upstream as g_sbi1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbi2 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (((Compiler.CompactSourceSyntax.synWsb y x ph).imp (Compiler.CompactSourceSyntax.synWsb y x ps)).imp (Compiler.CompactSourceSyntax.synWsb y x (ph.imp ps)))

Checked nominal proof certificate identified upstream as g_sbi2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbim (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x (ph.imp ps)) ((Compiler.CompactSourceSyntax.synWsb y x ph).imp (Compiler.CompactSourceSyntax.synWsb y x ps)))

Checked nominal proof certificate identified upstream as g_sbim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbor (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x (Compiler.CompactSourceSyntax.synWo ph ps)) (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWsb y x ph) (Compiler.CompactSourceSyntax.synWsb y x ps)))

Checked nominal proof certificate identified upstream as g_sbor.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSban (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWsb y x ph) (Compiler.CompactSourceSyntax.synWsb y x ps)))

Checked nominal proof certificate identified upstream as g_sban.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbbi (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x (Compiler.CompactSourceSyntax.synWb ph ps)) (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ph) (Compiler.CompactSourceSyntax.synWsb y x ps)))

Checked nominal proof certificate identified upstream as g_sbbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSblbis (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_sblbis_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ph) ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x (Compiler.CompactSourceSyntax.synWb ch ph)) (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ch) ps))

Checked nominal proof certificate identified upstream as g_sblbis.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfsb4t (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWnf z ph)).imp ((SemanticCore.Wff.all z (SemanticCore.Wff.objEq z y)).neg.imp (Compiler.CompactSourceSyntax.synWnf z (Compiler.CompactSourceSyntax.synWsb y x ph))))

Checked nominal proof certificate identified upstream as g_nfsb4t.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfsb4 (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (hyp_nfsb4_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z ph)) : Nominal.NPrf ((SemanticCore.Wff.all z (SemanticCore.Wff.objEq z y)).neg.imp (Compiler.CompactSourceSyntax.synWnf z (Compiler.CompactSourceSyntax.synWsb y x ph)))

Checked nominal proof certificate identified upstream as g_nfsb4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDvelimdf (ph ps ch : SemanticCore.Wff) (x y z : SemanticCore.Var) (hyp_dvelimdf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_dvelimdf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z ph)) (hyp_dvelimdf_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) (hyp_dvelimdf_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf z ch))) (hyp_dvelimdf_5 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.objEq z y).imp (Compiler.CompactSourceSyntax.synWb ps ch)))) : Nominal.NPrf (ph.imp ((SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y)).neg.imp (Compiler.CompactSourceSyntax.synWnf x ch)))

Checked nominal proof certificate identified upstream as g_dvelimdf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbco (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x (Compiler.CompactSourceSyntax.synWsb x y ph)) (Compiler.CompactSourceSyntax.synWsb y x ph))

Checked nominal proof certificate identified upstream as g_sbco.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbid2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_sbid2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x (Compiler.CompactSourceSyntax.synWsb x y ph)) ph)

Checked nominal proof certificate identified upstream as g_sbid2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbco2 (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (hyp_sbco2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y z (Compiler.CompactSourceSyntax.synWsb z x ph)) (Compiler.CompactSourceSyntax.synWsb y x ph))

Checked nominal proof certificate identified upstream as g_sbco2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSb6rf (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_sb5rf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (SemanticCore.Wff.all y ((SemanticCore.Wff.objEq y x).imp (Compiler.CompactSourceSyntax.synWsb y x ph))))

Checked nominal proof certificate identified upstream as g_sb6rf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSb8 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_sb5rf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ph) (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWsb y x ph)))

Checked nominal proof certificate identified upstream as g_sb8.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAx11v (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (ph.imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph))))

Checked nominal proof certificate identified upstream as g_ax11v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSb56 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x y) ph)) (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph)))

Checked nominal proof certificate identified upstream as g_sb56.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSb6 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ph) (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp ph)))

Checked nominal proof certificate identified upstream as g_sb6.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSb5 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ph) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objEq x y) ph)))

Checked nominal proof certificate identified upstream as g_sb5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqusb3lem (x y z : SemanticCore.Var) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x (SemanticCore.Wff.objEq x z)) (SemanticCore.Wff.objEq y z))

Checked nominal proof certificate identified upstream as g_equsb3lem.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqusb3 (x y z : SemanticCore.Var) (dv_x_z : x ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x (SemanticCore.Wff.objEq x z)) (SemanticCore.Wff.objEq y z))

Checked nominal proof certificate identified upstream as g_equsb3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbs1 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWsb y x ph).imp (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWsb y x ph)))

Checked nominal proof certificate identified upstream as g_hbs1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfs1v (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWsb y x ph))

Checked nominal proof certificate identified upstream as g_nfs1v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfsb (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_y_z : y ≠ z) (hyp_nfsb_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf z (Compiler.CompactSourceSyntax.synWsb y x ph))

Checked nominal proof certificate identified upstream as g_nfsb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbsb (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_y_z : y ≠ z) (hyp_hbsb_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all z ph))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWsb y x ph).imp (SemanticCore.Wff.all z (Compiler.CompactSourceSyntax.synWsb y x ph)))

Checked nominal proof certificate identified upstream as g_hbsb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfsbd (ph ps : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_y_z : y ≠ z) (hyp_nfsbd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_nfsbd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf z ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf z (Compiler.CompactSourceSyntax.synWsb y x ps)))

Checked nominal proof certificate identified upstream as g_nfsbd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEuf (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) (hyp_euf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x ph) (Compiler.CompactSourceSyntax.synWex y (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_euf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEubid (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_eubid_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_eubid_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x ps) (Compiler.CompactSourceSyntax.synWeu x ch)))

Checked nominal proof certificate identified upstream as g_eubid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEubidv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (hyp_eubidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x ps) (Compiler.CompactSourceSyntax.synWeu x ch)))

Checked nominal proof certificate identified upstream as g_eubidv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gEubidv ph ps ch x dv_ph_x hyp_eubidv_1 = NFChoice.DirectNominalPrf.WPPReplay.gEubid ph ps ch x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ph x ⋯) hyp_eubidv_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEubii (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_eubii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x ph) (Compiler.CompactSourceSyntax.synWeu x ps))

Checked nominal proof certificate identified upstream as g_eubii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfeu1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWeu x ph))

Checked nominal proof certificate identified upstream as g_nfeu1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfmo1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWmo x ph))

Checked nominal proof certificate identified upstream as g_nfmo1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfeud2 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfeud2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_nfeud2_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.synWnf x (Compiler.CompactSourceSyntax.synWeu y ps)))

Checked nominal proof certificate identified upstream as g_nfeud2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfmod2 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfeud2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_nfeud2_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.synWnf x (Compiler.CompactSourceSyntax.synWmo y ps)))

Checked nominal proof certificate identified upstream as g_nfmod2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfmod (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfeud_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_nfeud_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWmo y ps)))

Checked nominal proof certificate identified upstream as g_nfmod.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfmo (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfeu_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWmo y ph))

Checked nominal proof certificate identified upstream as g_nfmo.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSb8eu (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_sb8eu_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x ph) (Compiler.CompactSourceSyntax.synWeu y (Compiler.CompactSourceSyntax.synWsb y x ph)))

Checked nominal proof certificate identified upstream as g_sb8eu.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbveu (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_cbveu_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_cbveu_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbveu_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x ph) (Compiler.CompactSourceSyntax.synWeu y ps))

Checked nominal proof certificate identified upstream as g_cbveu.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEu1 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) (hyp_eu1_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x ph) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.all y ((Compiler.CompactSourceSyntax.synWsb y x ph).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))))))

Checked nominal proof certificate identified upstream as g_eu1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMo (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) (hyp_mo_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex y (SemanticCore.Wff.all x (ph.imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))) (SemanticCore.Wff.all x (SemanticCore.Wff.all y ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWsb y x ph)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_mo.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEuex (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWeu x ph).imp (Compiler.CompactSourceSyntax.synWex x ph))

Checked nominal proof certificate identified upstream as g_euex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEumo0 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) (hyp_eumo0_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWeu x ph).imp (Compiler.CompactSourceSyntax.synWex y (SemanticCore.Wff.all x (ph.imp (SemanticCore.Wff.objEq x y)))))

Checked nominal proof certificate identified upstream as g_eumo0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEu2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) (hyp_eu2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x ph) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x ph) (SemanticCore.Wff.all x (SemanticCore.Wff.all y ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWsb y x ph)).imp (SemanticCore.Wff.objEq x y))))))

Checked nominal proof certificate identified upstream as g_eu2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEu3 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) (hyp_eu3_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x ph) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWex y (SemanticCore.Wff.all x (ph.imp (SemanticCore.Wff.objEq x y))))))

Checked nominal proof certificate identified upstream as g_eu3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMo2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) (hyp_mo2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWmo x ph) (Compiler.CompactSourceSyntax.synWex y (SemanticCore.Wff.all x (ph.imp (SemanticCore.Wff.objEq x y)))))

Checked nominal proof certificate identified upstream as g_mo2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMo3 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) (hyp_mo3_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWmo x ph) (SemanticCore.Wff.all x (SemanticCore.Wff.all y ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWsb y x ph)).imp (SemanticCore.Wff.objEq x y)))))

Checked nominal proof certificate identified upstream as g_mo3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMo4f (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) (hyp_mo4f_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_mo4f_2 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWmo x ph) (SemanticCore.Wff.all x (SemanticCore.Wff.all y ((Compiler.CompactSourceSyntax.synWa ph ps).imp (SemanticCore.Wff.objEq x y)))))

Checked nominal proof certificate identified upstream as g_mo4f.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMo4 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_mo4_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWmo x ph) (SemanticCore.Wff.all x (SemanticCore.Wff.all y ((Compiler.CompactSourceSyntax.synWa ph ps).imp (SemanticCore.Wff.objEq x y)))))

Checked nominal proof certificate identified upstream as g_mo4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMobid (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_mobid_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_mobid_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWmo x ps) (Compiler.CompactSourceSyntax.synWmo x ch)))

Checked nominal proof certificate identified upstream as g_mobid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMobidv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (hyp_mobidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWmo x ps) (Compiler.CompactSourceSyntax.synWmo x ch)))

Checked nominal proof certificate identified upstream as g_mobidv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMobidv ph ps ch x dv_ph_x hyp_mobidv_1 = NFChoice.DirectNominalPrf.WPPReplay.gMobid ph ps ch x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ph x ⋯) hyp_mobidv_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMobii (ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_mobii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ch)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWmo x ps) (Compiler.CompactSourceSyntax.synWmo x ch))

Checked nominal proof certificate identified upstream as g_mobii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvmo (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_cbvmo_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_cbvmo_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbvmo_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWmo x ph) (Compiler.CompactSourceSyntax.synWmo y ps))

Checked nominal proof certificate identified upstream as g_cbvmo.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEu5 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x ph) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWmo x ph)))

Checked nominal proof certificate identified upstream as g_eu5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEu4 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_eu4_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x ph) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex x ph) (SemanticCore.Wff.all x (SemanticCore.Wff.all y ((Compiler.CompactSourceSyntax.synWa ph ps).imp (SemanticCore.Wff.objEq x y))))))

Checked nominal proof certificate identified upstream as g_eu4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEumo (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWeu x ph).imp (Compiler.CompactSourceSyntax.synWmo x ph))

Checked nominal proof certificate identified upstream as g_eumo.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExmoeu2 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex x ph).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWmo x ph) (Compiler.CompactSourceSyntax.synWeu x ph)))

Checked nominal proof certificate identified upstream as g_exmoeu2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExmo (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWex x ph) (Compiler.CompactSourceSyntax.synWmo x ph))

Checked nominal proof certificate identified upstream as g_exmo.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMoim (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (ph.imp ps)).imp ((Compiler.CompactSourceSyntax.synWmo x ps).imp (Compiler.CompactSourceSyntax.synWmo x ph)))

Checked nominal proof certificate identified upstream as g_moim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMoanim (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_moanim_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWmo x (Compiler.CompactSourceSyntax.synWa ph ps)) (ph.imp (Compiler.CompactSourceSyntax.synWmo x ps)))

Checked nominal proof certificate identified upstream as g_moanim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEuan (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_moanim_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x (Compiler.CompactSourceSyntax.synWa ph ps)) (Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWeu x ps)))

Checked nominal proof certificate identified upstream as g_euan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMoanimv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWmo x (Compiler.CompactSourceSyntax.synWa ph ps)) (ph.imp (Compiler.CompactSourceSyntax.synWmo x ps)))

Checked nominal proof certificate identified upstream as g_moanimv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMoanimv ph ps x dv_ph_x = NFChoice.DirectNominalPrf.WPPReplay.gMoanim ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ph x ⋯)

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

Checked nominal proof certificate identified upstream as g_euanv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gEuanv ph ps x dv_ph_x = NFChoice.DirectNominalPrf.WPPReplay.gEuan ph ps x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ph x ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMopick (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWmo x ph) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps))).imp (ph.imp ps))

Checked nominal proof certificate identified upstream as g_mopick.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEupick (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWeu x ph) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps))).imp (ph.imp ps))

Checked nominal proof certificate identified upstream as g_eupick.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMoexex (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_moexex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWmo x ph) (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWmo y ps))).imp (Compiler.CompactSourceSyntax.synWmo y (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps))))

Checked nominal proof certificate identified upstream as g_moexex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMoexexv (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_y : y ∉ ph.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWmo x ph) (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWmo y ps))).imp (Compiler.CompactSourceSyntax.synWmo y (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ph ps))))

Checked nominal proof certificate identified upstream as g_moexexv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gMoexexv ph ps x y dv_ph_y = NFChoice.DirectNominalPrf.WPPReplay.gMoexex ph ps x y (NFChoice.DirectNominalPrf.WPPReplay.gNfv ph y ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEuequ1 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWeu x (SemanticCore.Wff.objEq x y))

Checked nominal proof certificate identified upstream as g_euequ1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAbid (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cab x ph)) ph)

Checked nominal proof certificate identified upstream as g_abid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbab1 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (SemanticCore.Class.cab x ph)).imp (SemanticCore.Wff.all x (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (SemanticCore.Class.cab x ph))))

Checked nominal proof certificate identified upstream as g_hbab1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfsab1 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (SemanticCore.Class.cab x ph)))

Checked nominal proof certificate identified upstream as g_nfsab1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHbab (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_x_z : x ≠ z) (hyp_hbab_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.all x ph))) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv z) (SemanticCore.Class.cab y ph)).imp (SemanticCore.Wff.all x (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) (SemanticCore.Class.cab y ph))))

Checked nominal proof certificate identified upstream as g_hbab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfsab (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (dv_x_z : x ≠ z) (hyp_nfsab_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) (SemanticCore.Class.cab y ph)))

Checked nominal proof certificate identified upstream as g_nfsab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfcleq (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.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_dfcleq.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqriv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqrdv (ph : 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_eqrdv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B)))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_eqrdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqid (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq A A)

Checked nominal proof certificate identified upstream as g_eqid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqidd (ph : SemanticCore.Wff) (A : SemanticCore.Class) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A A))

Checked nominal proof certificate identified upstream as g_eqidd.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gEqidd ph A = NFChoice.DirectNominalPrf.WPPReplay.gA1i (NFChoice.SemanticCore.Wff.classEq A A) ph (NFChoice.DirectNominalPrf.WPPReplay.gEqid A)

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

Checked nominal proof certificate identified upstream as g_eqcom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqcoms (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_eqcoms_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp ph)) : Nominal.NPrf ((SemanticCore.Wff.classEq B A).imp ph)

Checked nominal proof certificate identified upstream as g_eqcoms.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqcomi (A B : SemanticCore.Class) (hyp_eqcomi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq B A)

Checked nominal proof certificate identified upstream as g_eqcomi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqcomd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_eqcomd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B A))

Checked nominal proof certificate identified upstream as g_eqcomd.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqeq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqeq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gEqeq1i A B C hyp_eqeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_eqeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gEqeq1 A B C)

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

Checked nominal proof certificate identified upstream as g_eqeq1d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqeq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqeq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gEqeq2i A B C hyp_eqeq2i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_eqeq2i_1 (NFChoice.DirectNominalPrf.WPPReplay.gEqeq2 A B C)

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

Checked nominal proof certificate identified upstream as g_eqeq2d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqeq12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqeq12i (A B C D : SemanticCore.Class) (hyp_eqeq12i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_eqeq12i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A C) (SemanticCore.Wff.classEq B D))

Checked nominal proof certificate identified upstream as g_eqeq12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqeq12d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_eqeq12d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqeq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A C) (SemanticCore.Wff.classEq B D)))

Checked nominal proof certificate identified upstream as g_eqeq12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqeqan12d (ph ps : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_eqeqan12d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqeqan12d_2 : Nominal.NPrf (ps.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A C) (SemanticCore.Wff.classEq B D)))

Checked nominal proof certificate identified upstream as g_eqeqan12d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqtr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqtr2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqtr3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqtri (A B C : SemanticCore.Class) (hyp_eqtri_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_eqtri_2 : Nominal.NPrf (SemanticCore.Wff.classEq B C)) : Nominal.NPrf (SemanticCore.Wff.classEq A C)

Checked nominal proof certificate identified upstream as g_eqtri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqtr2i (A B C : SemanticCore.Class) (hyp_eqtr2i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_eqtr2i_2 : Nominal.NPrf (SemanticCore.Wff.classEq B C)) : Nominal.NPrf (SemanticCore.Wff.classEq C A)

Checked nominal proof certificate identified upstream as g_eqtr2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqtr3i (A B C : SemanticCore.Class) (hyp_eqtr3i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_eqtr3i_2 : Nominal.NPrf (SemanticCore.Wff.classEq A C)) : Nominal.NPrf (SemanticCore.Wff.classEq B C)

Checked nominal proof certificate identified upstream as g_eqtr3i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqtr4i (A B C : SemanticCore.Class) (hyp_eqtr4i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_eqtr4i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C B)) : Nominal.NPrf (SemanticCore.Wff.classEq A C)

Checked nominal proof certificate identified upstream as g_eqtr4i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtri (A B C D : SemanticCore.Class) (hyp_n_3eqtri_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_n_3eqtri_2 : Nominal.NPrf (SemanticCore.Wff.classEq B C)) (hyp_n_3eqtri_3 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (SemanticCore.Wff.classEq A D)

Checked nominal proof certificate identified upstream as g_n_3eqtri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtrri (A B C D : SemanticCore.Class) (hyp_n_3eqtri_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_n_3eqtri_2 : Nominal.NPrf (SemanticCore.Wff.classEq B C)) (hyp_n_3eqtri_3 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (SemanticCore.Wff.classEq D A)

Checked nominal proof certificate identified upstream as g_n_3eqtrri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtr2i (A B C D : SemanticCore.Class) (hyp_n_3eqtr2i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_n_3eqtr2i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C B)) (hyp_n_3eqtr2i_3 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (SemanticCore.Wff.classEq A D)

Checked nominal proof certificate identified upstream as g_n_3eqtr2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtr2ri (A B C D : SemanticCore.Class) (hyp_n_3eqtr2i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_n_3eqtr2i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C B)) (hyp_n_3eqtr2i_3 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (SemanticCore.Wff.classEq D A)

Checked nominal proof certificate identified upstream as g_n_3eqtr2ri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtr3i (A B C D : SemanticCore.Class) (hyp_n_3eqtr3i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_n_3eqtr3i_2 : Nominal.NPrf (SemanticCore.Wff.classEq A C)) (hyp_n_3eqtr3i_3 : Nominal.NPrf (SemanticCore.Wff.classEq B D)) : Nominal.NPrf (SemanticCore.Wff.classEq C D)

Checked nominal proof certificate identified upstream as g_n_3eqtr3i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtr4i (A B C D : SemanticCore.Class) (hyp_n_3eqtr4i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_n_3eqtr4i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C A)) (hyp_n_3eqtr4i_3 : Nominal.NPrf (SemanticCore.Wff.classEq D B)) : Nominal.NPrf (SemanticCore.Wff.classEq C D)

Checked nominal proof certificate identified upstream as g_n_3eqtr4i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtr4ri (A B C D : SemanticCore.Class) (hyp_n_3eqtr4i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_n_3eqtr4i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C A)) (hyp_n_3eqtr4i_3 : Nominal.NPrf (SemanticCore.Wff.classEq D B)) : Nominal.NPrf (SemanticCore.Wff.classEq D C)

Checked nominal proof certificate identified upstream as g_n_3eqtr4ri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqtrd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eqtrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqtrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A C))

Checked nominal proof certificate identified upstream as g_eqtrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqtr2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eqtr2d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqtr2d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C A))

Checked nominal proof certificate identified upstream as g_eqtr2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqtr3d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eqtr3d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqtr3d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))

Checked nominal proof certificate identified upstream as g_eqtr3d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqtr4d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eqtr4d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqtr4d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A C))

Checked nominal proof certificate identified upstream as g_eqtr4d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtrd (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_n_3eqtrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_n_3eqtrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) (hyp_n_3eqtrd_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A D))

Checked nominal proof certificate identified upstream as g_n_3eqtrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtr3d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_n_3eqtr3d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_n_3eqtr3d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A C))) (hyp_n_3eqtr3d_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B D))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))

Checked nominal proof certificate identified upstream as g_n_3eqtr3d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtr4d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_n_3eqtr4d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_n_3eqtr4d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C A))) (hyp_n_3eqtr4d_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq D B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))

Checked nominal proof certificate identified upstream as g_n_3eqtr4d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5eq (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5eq_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_syl5eq_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A C))

Checked nominal proof certificate identified upstream as g_syl5eq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5req (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5req_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_syl5req_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C A))

Checked nominal proof certificate identified upstream as g_syl5req.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5eqr (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5eqr_1 : Nominal.NPrf (SemanticCore.Wff.classEq B A)) (hyp_syl5eqr_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A C))

Checked nominal proof certificate identified upstream as g_syl5eqr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5reqr (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5reqr_1 : Nominal.NPrf (SemanticCore.Wff.classEq B A)) (hyp_syl5reqr_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C A))

Checked nominal proof certificate identified upstream as g_syl5reqr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6eq (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl6eq_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_syl6eq_2 : Nominal.NPrf (SemanticCore.Wff.classEq B C)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A C))

Checked nominal proof certificate identified upstream as g_syl6eq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6req (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl6req_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_syl6req_2 : Nominal.NPrf (SemanticCore.Wff.classEq B C)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C A))

Checked nominal proof certificate identified upstream as g_syl6req.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6eqr (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl6eqr_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_syl6eqr_2 : Nominal.NPrf (SemanticCore.Wff.classEq C B)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A C))

Checked nominal proof certificate identified upstream as g_syl6eqr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6reqr (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl6reqr_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_syl6reqr_2 : Nominal.NPrf (SemanticCore.Wff.classEq C B)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C A))

Checked nominal proof certificate identified upstream as g_syl6reqr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan9eq (ph ps : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_sylan9eq_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_sylan9eq_2 : Nominal.NPrf (ps.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (SemanticCore.Wff.classEq A C))

Checked nominal proof certificate identified upstream as g_sylan9eq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan9eqr (ph ps : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_sylan9eqr_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_sylan9eqr_2 : Nominal.NPrf (ps.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ph).imp (SemanticCore.Wff.classEq A C))

Checked nominal proof certificate identified upstream as g_sylan9eqr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtr3g (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_n_3eqtr3g_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_n_3eqtr3g_2 : Nominal.NPrf (SemanticCore.Wff.classEq A C)) (hyp_n_3eqtr3g_3 : Nominal.NPrf (SemanticCore.Wff.classEq B D)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))

Checked nominal proof certificate identified upstream as g_n_3eqtr3g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtr4g (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_n_3eqtr4g_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_n_3eqtr4g_2 : Nominal.NPrf (SemanticCore.Wff.classEq C A)) (hyp_n_3eqtr4g_3 : Nominal.NPrf (SemanticCore.Wff.classEq D B)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))

Checked nominal proof certificate identified upstream as g_n_3eqtr4g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3eqtr4a (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_n_3eqtr4a_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_n_3eqtr4a_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C A))) (hyp_n_3eqtr4a_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq D B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))

Checked nominal proof certificate identified upstream as g_n_3eqtr4a.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eleq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eleq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEleq12 (A B C D : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.classEq C D)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)))

Checked nominal proof certificate identified upstream as g_eleq12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEleq1i (A B C : SemanticCore.Class) (hyp_eleq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B C))

Checked nominal proof certificate identified upstream as g_eleq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gEleq1i A B C hyp_eleq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_eleq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gEleq1 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEleq2i (A B C : SemanticCore.Class) (hyp_eleq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C A) (SemanticCore.Wff.classMem C B))

Checked nominal proof certificate identified upstream as g_eleq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gEleq2i A B C hyp_eleq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_eleq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gEleq2 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEleq1d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eleq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B C)))

Checked nominal proof certificate identified upstream as g_eleq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEleq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eleq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C A) (SemanticCore.Wff.classMem C B)))

Checked nominal proof certificate identified upstream as g_eleq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEleq1a (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A B).imp ((SemanticCore.Wff.classEq C A).imp (SemanticCore.Wff.classMem C B)))

Checked nominal proof certificate identified upstream as g_eleq1a.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqeltri (A B C : SemanticCore.Class) (hyp_eqeltr_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_eqeltr_2 : Nominal.NPrf (SemanticCore.Wff.classMem B C)) : Nominal.NPrf (SemanticCore.Wff.classMem A C)

Checked nominal proof certificate identified upstream as g_eqeltri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqeltrri (A B C : SemanticCore.Class) (hyp_eqeltrr_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_eqeltrr_2 : Nominal.NPrf (SemanticCore.Wff.classMem A C)) : Nominal.NPrf (SemanticCore.Wff.classMem B C)

Checked nominal proof certificate identified upstream as g_eqeltrri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEleqtri (A B C : SemanticCore.Class) (hyp_eleqtr_1 : Nominal.NPrf (SemanticCore.Wff.classMem A B)) (hyp_eleqtr_2 : Nominal.NPrf (SemanticCore.Wff.classEq B C)) : Nominal.NPrf (SemanticCore.Wff.classMem A C)

Checked nominal proof certificate identified upstream as g_eleqtri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEleqtrri (A B C : SemanticCore.Class) (hyp_eleqtrr_1 : Nominal.NPrf (SemanticCore.Wff.classMem A B)) (hyp_eleqtrr_2 : Nominal.NPrf (SemanticCore.Wff.classEq C B)) : Nominal.NPrf (SemanticCore.Wff.classMem A C)

Checked nominal proof certificate identified upstream as g_eleqtrri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqeltrd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eqeltrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqeltrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A C))

Checked nominal proof certificate identified upstream as g_eqeltrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqeltrrd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eqeltrrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqeltrrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem B C))

Checked nominal proof certificate identified upstream as g_eqeltrrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEleqtrd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eleqtrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A B))) (hyp_eleqtrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A C))

Checked nominal proof certificate identified upstream as g_eleqtrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEleqtrrd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eleqtrrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A B))) (hyp_eleqtrrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A C))

Checked nominal proof certificate identified upstream as g_eleqtrrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5eqel (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5eqel_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_syl5eqel_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A C))

Checked nominal proof certificate identified upstream as g_syl5eqel.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5eqelr (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5eqelr_1 : Nominal.NPrf (SemanticCore.Wff.classEq B A)) (hyp_syl5eqelr_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A C))

Checked nominal proof certificate identified upstream as g_syl5eqelr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5eleq (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5eleq_1 : Nominal.NPrf (SemanticCore.Wff.classMem A B)) (hyp_syl5eleq_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A C))

Checked nominal proof certificate identified upstream as g_syl5eleq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5eleqr (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5eleqr_1 : Nominal.NPrf (SemanticCore.Wff.classMem A B)) (hyp_syl5eleqr_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A C))

Checked nominal proof certificate identified upstream as g_syl5eleqr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6eqel (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl6eqel_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_syl6eqel_2 : Nominal.NPrf (SemanticCore.Wff.classMem B C)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A C))

Checked nominal proof certificate identified upstream as g_syl6eqel.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6eqelr (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl6eqelr_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B A))) (hyp_syl6eqelr_2 : Nominal.NPrf (SemanticCore.Wff.classMem B C)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A C))

Checked nominal proof certificate identified upstream as g_syl6eqelr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6eleq (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl6eleq_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A B))) (hyp_syl6eleq_2 : Nominal.NPrf (SemanticCore.Wff.classEq B C)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A C))

Checked nominal proof certificate identified upstream as g_syl6eleq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6eleqr (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl6eleqr_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A B))) (hyp_syl6eleqr_2 : Nominal.NPrf (SemanticCore.Wff.classEq C B)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A C))

Checked nominal proof certificate identified upstream as g_syl6eleqr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEleq2s (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eleq2s_1 : Nominal.NPrf ((SemanticCore.Wff.classMem A B).imp ph)) (hyp_eleq2s_2 : Nominal.NPrf (SemanticCore.Wff.classEq C B)) : Nominal.NPrf ((SemanticCore.Wff.classMem A C).imp ph)

Checked nominal proof certificate identified upstream as g_eleq2s.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNeleqtrd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_neleqtrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem C A).neg)) (hyp_neleqtrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem C B).neg)

Checked nominal proof certificate identified upstream as g_neleqtrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCleqh (x y : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) (hyp_cleqh_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A).imp (SemanticCore.Wff.all x (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A)))) (hyp_cleqh_2 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B).imp (SemanticCore.Wff.all x (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) 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_cleqh.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqsb1lem (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) A))

Checked nominal proof certificate identified upstream as g_eqsb1lem.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqsb1 (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) A))

Checked nominal proof certificate identified upstream as g_eqsb1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClelsb1 (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A))

Checked nominal proof certificate identified upstream as g_clelsb1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHblem (x y z : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_x_z : x ≠ z) (hyp_hblem_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A).imp (SemanticCore.Wff.all x (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A)))) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv z) A).imp (SemanticCore.Wff.all x (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) A)))

Checked nominal proof certificate identified upstream as g_hblem.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqabb (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A (SemanticCore.Class.cab x ph)) (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph)))

Checked nominal proof certificate identified upstream as g_eqabb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqabcb (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ph) A) (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A))))

Checked nominal proof certificate identified upstream as g_eqabcb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqabri (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_eqabri_1 : Nominal.NPrf (SemanticCore.Wff.classEq A (SemanticCore.Class.cab x ph))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph)

Checked nominal proof certificate identified upstream as g_eqabri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqabrd (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_eqabrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A (SemanticCore.Class.cab x ps)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ps))

Checked nominal proof certificate identified upstream as g_eqabrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAbbib (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ph) (SemanticCore.Class.cab x ps)) (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb ph ps)))

Checked nominal proof certificate identified upstream as g_abbib.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqabi (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_abbiri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph)) : Nominal.NPrf (SemanticCore.Wff.classEq A (SemanticCore.Class.cab x ph))

Checked nominal proof certificate identified upstream as g_eqabi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAbbii (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_abbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ph) (SemanticCore.Class.cab x ps))

Checked nominal proof certificate identified upstream as g_abbii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAbbid (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_abbid_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_abbid_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ps) (SemanticCore.Class.cab x ch)))

Checked nominal proof certificate identified upstream as g_abbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAbbidv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (hyp_abbidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ps) (SemanticCore.Class.cab x ch)))

Checked nominal proof certificate identified upstream as g_abbidv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAbbidv ph ps ch x dv_ph_x hyp_abbidv_1 = NFChoice.DirectNominalPrf.WPPReplay.gAbbid ph ps ch x (NFChoice.DirectNominalPrf.WPPReplay.gNfv ph x ⋯) hyp_abbidv_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqabdv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ph_x : x ∉ ph.fv) (hyp_eqabdv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ps))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A (SemanticCore.Class.cab x ps)))

Checked nominal proof certificate identified upstream as g_eqabdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqabcdv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ph_x : x ∉ ph.fv) (hyp_eqabcdv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ps) A))

Checked nominal proof certificate identified upstream as g_eqabcdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAbid2 (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (SemanticCore.Class.cab x (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)) A)

Checked nominal proof certificate identified upstream as g_abid2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCbvab (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_cbvab_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_cbvab_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_cbvab_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ph) (SemanticCore.Class.cab y ps))

Checked nominal proof certificate identified upstream as g_cbvab.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nfci.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nfcr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcrii (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_x_y : x ≠ y) (hyp_nfcri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A).imp (SemanticCore.Wff.all x (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A)))

Checked nominal proof certificate identified upstream as g_nfcrii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcri (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_x_y : x ≠ y) (hyp_nfcri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) A))

Checked nominal proof certificate identified upstream as g_nfcri.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nfcd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfceqi (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfceqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWnfc x A) (Compiler.CompactSourceSyntax.synWnfc x B))

Checked nominal proof certificate identified upstream as g_nfceqi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcxfr (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfceqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_nfcxfr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)

Checked nominal proof certificate identified upstream as g_nfcxfr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcxfrd (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfceqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_nfcxfrd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))

Checked nominal proof certificate identified upstream as g_nfcxfrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfceqdf (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfceqdf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_nfceqdf_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWnfc x A) (Compiler.CompactSourceSyntax.synWnfc x B)))

Checked nominal proof certificate identified upstream as g_nfceqdf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcv (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)

Checked nominal proof certificate identified upstream as g_nfcv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcvd (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))

Checked nominal proof certificate identified upstream as g_nfcvd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfab1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (SemanticCore.Class.cab x ph))

Checked nominal proof certificate identified upstream as g_nfab1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfnfc1 (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWnfc x A))

Checked nominal proof certificate identified upstream as g_nfnfc1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfab (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (hyp_nfab_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (SemanticCore.Class.cab y ph))

Checked nominal proof certificate identified upstream as g_nfab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfaba1 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (SemanticCore.Class.cab y (SemanticCore.Wff.all x ph)))

Checked nominal proof certificate identified upstream as g_nfaba1.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNfaba1 ph x y = NFChoice.DirectNominalPrf.WPPReplay.gNfab (NFChoice.SemanticCore.Wff.all x ph) x y (NFChoice.DirectNominalPrf.WPPReplay.gNfa1 ph x)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfeq (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfnfc_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_nfeq_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_nfeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfel (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfnfc_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_nfeq_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.classMem A B))

Checked nominal proof certificate identified upstream as g_nfel.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfel1 (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_B_x : x ∉ B.fv) (hyp_nfeq1_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.classMem A B))

Checked nominal proof certificate identified upstream as g_nfel1.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNfel1 x A B dv_B_x hyp_nfeq1_1 = NFChoice.DirectNominalPrf.WPPReplay.gNfel x A B hyp_nfeq1_1 (NFChoice.DirectNominalPrf.WPPReplay.gNfcv x B ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfeq2 (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_nfeq2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_nfeq2.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNfeq2 x A B dv_A_x hyp_nfeq2_1 = NFChoice.DirectNominalPrf.WPPReplay.gNfeq x A B (NFChoice.DirectNominalPrf.WPPReplay.gNfcv x A ⋯) hyp_nfeq2_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfel2 (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_nfeq2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x (SemanticCore.Wff.classMem A B))

Checked nominal proof certificate identified upstream as g_nfel2.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNfel2 x A B dv_A_x hyp_nfeq2_1 = NFChoice.DirectNominalPrf.WPPReplay.gNfel x A B (NFChoice.DirectNominalPrf.WPPReplay.gNfcv x A ⋯) hyp_nfeq2_1