NF weak partition development: NominalWPPReplayChunk002.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm55 (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (ph.imp ps) ps))

Checked nominal proof certificate identified upstream as g_pm5_5.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm55 ph ps = NFChoice.DirectNominalPrf.WPPReplay.gBicomd ph ps (ph.imp ps) (NFChoice.DirectNominalPrf.WPPReplay.gBiimt ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gA1bi (ph ps : SemanticCore.Wff) (hyp_a1bi_1 : Nominal.NPrf ph) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps (ph.imp ps))

Checked nominal proof certificate identified upstream as g_a1bi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gA1bi ph ps hyp_a1bi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_a1bi_1 (NFChoice.DirectNominalPrf.WPPReplay.gBiimt ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm5501 (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps (Compiler.CompactSourceSyntax.synWb ph ps)))

Checked nominal proof certificate identified upstream as g_pm5_501.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIbibr (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps) (ph.imp (Compiler.CompactSourceSyntax.synWb ps ph)))

Checked nominal proof certificate identified upstream as g_ibibr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTbt (ph ps : SemanticCore.Wff) (hyp_tbt_1 : Nominal.NPrf ph) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps (Compiler.CompactSourceSyntax.synWb ps ph))

Checked nominal proof certificate identified upstream as g_tbt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNbn2 (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.neg.imp (Compiler.CompactSourceSyntax.synWb ps.neg (Compiler.CompactSourceSyntax.synWb ph ps)))

Checked nominal proof certificate identified upstream as g_nbn2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBibif (ph ps : SemanticCore.Wff) : Nominal.NPrf (ps.neg.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ph ps) ph.neg))

Checked nominal proof certificate identified upstream as g_bibif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNbn (ph ps : SemanticCore.Wff) (hyp_nbn_1 : Nominal.NPrf ph.neg) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps.neg (Compiler.CompactSourceSyntax.synWb ps ph))

Checked nominal proof certificate identified upstream as g_nbn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm521im (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.neg.imp (ps.neg.imp (Compiler.CompactSourceSyntax.synWb ph ps)))

Checked nominal proof certificate identified upstream as g_pm5_21im.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2false (ph ps : SemanticCore.Wff) (hyp_n_2false_1 : Nominal.NPrf ph.neg) (hyp_n_2false_2 : Nominal.NPrf ps.neg) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)

Checked nominal proof certificate identified upstream as g_n_2false.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN2falsed (ph ps ch : SemanticCore.Wff) (hyp_n_2falsed_1 : Nominal.NPrf (ph.imp ps.neg)) (hyp_n_2falsed_2 : Nominal.NPrf (ph.imp ch.neg)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))

Checked nominal proof certificate identified upstream as g_n_2falsed.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm521ni (ph ps ch : SemanticCore.Wff) (hyp_pm5_21ni_1 : Nominal.NPrf (ph.imp ps)) (hyp_pm5_21ni_2 : Nominal.NPrf (ch.imp ps)) : Nominal.NPrf (ps.neg.imp (Compiler.CompactSourceSyntax.synWb ph ch))

Checked nominal proof certificate identified upstream as g_pm5_21ni.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm521nii (ph ps ch : SemanticCore.Wff) (hyp_pm5_21ni_1 : Nominal.NPrf (ph.imp ps)) (hyp_pm5_21ni_2 : Nominal.NPrf (ch.imp ps)) (hyp_pm5_21nii_3 : Nominal.NPrf (ps.imp (Compiler.CompactSourceSyntax.synWb ph ch))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ch)

Checked nominal proof certificate identified upstream as g_pm5_21nii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm521ndd (ph ps ch th : SemanticCore.Wff) (hyp_pm5_21ndd_1 : Nominal.NPrf (ph.imp (ch.imp ps))) (hyp_pm5_21ndd_2 : Nominal.NPrf (ph.imp (th.imp ps))) (hyp_pm5_21ndd_3 : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWb ch th)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch th))

Checked nominal proof certificate identified upstream as g_pm5_21ndd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm518 (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ph ps) (Compiler.CompactSourceSyntax.synWb ph ps.neg).neg)

Checked nominal proof certificate identified upstream as g_pm5_18.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm519 (ph : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ph.neg).neg

Checked nominal proof certificate identified upstream as g_pm5_19.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBi204 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp (ps.imp ch)) (ps.imp (ph.imp ch)))

Checked nominal proof certificate identified upstream as g_bi2_04.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm464 (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.neg.imp ps) (Compiler.CompactSourceSyntax.synWo ph ps))

Checked nominal proof certificate identified upstream as g_pm4_64.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm253 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWo ph ps).imp (ph.neg.imp ps))

Checked nominal proof certificate identified upstream as g_pm2_53.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm254 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((ph.neg.imp ps).imp (Compiler.CompactSourceSyntax.synWo ph ps))

Checked nominal proof certificate identified upstream as g_pm2_54.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOri (ph ps : SemanticCore.Wff) (hyp_ori_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWo ph ps)) : Nominal.NPrf (ph.neg.imp ps)

Checked nominal proof certificate identified upstream as g_ori.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrri (ph ps : SemanticCore.Wff) (hyp_orri_1 : Nominal.NPrf (ph.neg.imp ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWo ph ps)

Checked nominal proof certificate identified upstream as g_orri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrd (ph ps ch : SemanticCore.Wff) (hyp_ord_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo ps ch))) : Nominal.NPrf (ph.imp (ps.neg.imp ch))

Checked nominal proof certificate identified upstream as g_ord.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrrd (ph ps ch : SemanticCore.Wff) (hyp_orrd_1 : Nominal.NPrf (ph.imp (ps.neg.imp ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo ps ch))

Checked nominal proof certificate identified upstream as g_orrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJaoi (ph ps ch : SemanticCore.Wff) (hyp_jaoi_1 : Nominal.NPrf (ph.imp ps)) (hyp_jaoi_2 : Nominal.NPrf (ch.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWo ph ch).imp ps)

Checked nominal proof certificate identified upstream as g_jaoi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJaod (ph ps ch th : SemanticCore.Wff) (hyp_jaod_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_jaod_2 : Nominal.NPrf (ph.imp (th.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWo ps th).imp ch))

Checked nominal proof certificate identified upstream as g_jaod.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpjaod (ph ps ch th : SemanticCore.Wff) (hyp_jaod_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_jaod_2 : Nominal.NPrf (ph.imp (th.imp ch))) (hyp_jaod_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo ps th))) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_mpjaod.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrel1 (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.neg.imp ((Compiler.CompactSourceSyntax.synWo ph ps).imp ps))

Checked nominal proof certificate identified upstream as g_orel1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrel2 (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.neg.imp ((Compiler.CompactSourceSyntax.synWo ps ph).imp ps))

Checked nominal proof certificate identified upstream as g_orel2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOlc (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo ps ph))

Checked nominal proof certificate identified upstream as g_olc.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gOlc ph ps = NFChoice.DirectNominalPrf.WPPReplay.gOrrd ph ps ph (NFChoice.DirectNominalPrf.Nominal.ax1 ph ps.neg)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrc (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo ph ps))

Checked nominal proof certificate identified upstream as g_orc.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gOrc ph ps = NFChoice.DirectNominalPrf.WPPReplay.gOrrd ph ph ps (NFChoice.DirectNominalPrf.WPPReplay.gPm224 ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm14 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWo ph ps).imp (Compiler.CompactSourceSyntax.synWo ps ph))

Checked nominal proof certificate identified upstream as g_pm1_4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrcom (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo ph ps) (Compiler.CompactSourceSyntax.synWo ps ph))

Checked nominal proof certificate identified upstream as g_orcom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrcomd (ph ps ch : SemanticCore.Wff) (hyp_orcomd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo ch ps))

Checked nominal proof certificate identified upstream as g_orcomd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrci (ph ps : SemanticCore.Wff) (hyp_orci_1 : Nominal.NPrf ph) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWo ph ps)

Checked nominal proof certificate identified upstream as g_orci.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gOrci ph ps hyp_orci_1 = NFChoice.DirectNominalPrf.WPPReplay.gOrri ph ps (NFChoice.DirectNominalPrf.WPPReplay.gPm224i ph ps hyp_orci_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrcd (ph ps ch : SemanticCore.Wff) (hyp_orcd_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo ps ch))

Checked nominal proof certificate identified upstream as g_orcd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOlcd (ph ps ch : SemanticCore.Wff) (hyp_orcd_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo ch ps))

Checked nominal proof certificate identified upstream as g_olcd.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gOlcd ph ps ch hyp_orcd_1 = NFChoice.DirectNominalPrf.WPPReplay.gOrcomd ph ps ch (NFChoice.DirectNominalPrf.WPPReplay.gOrcd ph ps ch hyp_orcd_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm207 (ph : SemanticCore.Wff) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo ph ph))

Checked nominal proof certificate identified upstream as g_pm2_07.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm207 ph = NFChoice.DirectNominalPrf.WPPReplay.gOlc ph ph

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.g_pm2_67_2 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf (((Compiler.CompactSourceSyntax.synWo ph ch).imp ps).imp (ph.imp ps))

Checked nominal proof certificate identified upstream as g_pm2_67_2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiorf (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.neg.imp (Compiler.CompactSourceSyntax.synWb ps (Compiler.CompactSourceSyntax.synWo ph ps)))

Checked nominal proof certificate identified upstream as g_biorf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiorfi (ph ps : SemanticCore.Wff) (hyp_biorfi_1 : Nominal.NPrf ph.neg) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps (Compiler.CompactSourceSyntax.synWo ps ph))

Checked nominal proof certificate identified upstream as g_biorfi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm2621 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((ph.imp ps).imp ((Compiler.CompactSourceSyntax.synWo ph ps).imp ps))

Checked nominal proof certificate identified upstream as g_pm2_621.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImor (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps) (Compiler.CompactSourceSyntax.synWo ph.neg ps))

Checked nominal proof certificate identified upstream as g_imor.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExmid (ph : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWo ph ph.neg)

Checked nominal proof certificate identified upstream as g_exmid.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gExmid ph = NFChoice.DirectNominalPrf.WPPReplay.gOrri ph ph.neg (NFChoice.DirectNominalPrf.WPPReplay.gId ph.neg)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm462 (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps.neg) (Compiler.CompactSourceSyntax.synWo ph.neg ps.neg))

Checked nominal proof certificate identified upstream as g_pm4_62.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm462 ph ps = NFChoice.DirectNominalPrf.WPPReplay.gImor ph ps.neg

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImnan (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps.neg) (Compiler.CompactSourceSyntax.synWa ph ps).neg)

Checked nominal proof certificate identified upstream as g_imnan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIman (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps) (Compiler.CompactSourceSyntax.synWa ph ps.neg).neg)

Checked nominal proof certificate identified upstream as g_iman.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnnim (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph ps.neg) (ph.imp ps).neg)

Checked nominal proof certificate identified upstream as g_annim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm461 (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps).neg (Compiler.CompactSourceSyntax.synWa ph ps.neg))

Checked nominal proof certificate identified upstream as g_pm4_61.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm465 (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.neg.imp ps).neg (Compiler.CompactSourceSyntax.synWa ph.neg ps.neg))

Checked nominal proof certificate identified upstream as g_pm4_65.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm465 ph ps = NFChoice.DirectNominalPrf.WPPReplay.gPm461 ph.neg ps

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImp (ph ps ch : SemanticCore.Wff) (hyp_imp_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)

Checked nominal proof certificate identified upstream as g_imp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpcom (ph ps ch : SemanticCore.Wff) (hyp_imp_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ph).imp ch)

Checked nominal proof certificate identified upstream as g_impcom.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gImpcom ph ps ch hyp_imp_1 = NFChoice.DirectNominalPrf.WPPReplay.gImp ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gCom12 ph ps ch hyp_imp_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImp3a (ph ps ch th : SemanticCore.Wff) (hyp_imp3_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps ch).imp th))

Checked nominal proof certificate identified upstream as g_imp3a.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImp31 (ph ps ch th : SemanticCore.Wff) (hyp_imp3_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) ch).imp th)

Checked nominal proof certificate identified upstream as g_imp31.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImp32 (ph ps ch th : SemanticCore.Wff) (hyp_imp3_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ch)).imp th)

Checked nominal proof certificate identified upstream as g_imp32.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEx (ph ps ch : SemanticCore.Wff) (hyp_exp_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf (ph.imp (ps.imp ch))

Checked nominal proof certificate identified upstream as g_ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExpcom (ph ps ch : SemanticCore.Wff) (hyp_exp_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf (ps.imp (ph.imp ch))

Checked nominal proof certificate identified upstream as g_expcom.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gExpcom ph ps ch hyp_exp_1 = NFChoice.DirectNominalPrf.WPPReplay.gCom12 ph ps ch (NFChoice.DirectNominalPrf.WPPReplay.gEx ph ps ch hyp_exp_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExp3a (ph ps ch th : SemanticCore.Wff) (hyp_exp3a_1 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps ch).imp th))) : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))

Checked nominal proof certificate identified upstream as g_exp3a.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExpdimp (ph ps ch th : SemanticCore.Wff) (hyp_exp3a_1 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps ch).imp th))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (ch.imp th))

Checked nominal proof certificate identified upstream as g_expdimp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpancom (ph ps ch th : SemanticCore.Wff) (hyp_impancom_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (ch.imp th))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_impancom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCon3and (ph ps ch : SemanticCore.Wff) (hyp_con3and_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch.neg).imp ps.neg)

Checked nominal proof certificate identified upstream as g_con3and.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm201da (ph ps : SemanticCore.Wff) (hyp_pm2_01da_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ps.neg)) : Nominal.NPrf (ph.imp ps.neg)

Checked nominal proof certificate identified upstream as g_pm2_01da.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm201da ph ps hyp_pm2_01da_1 = NFChoice.DirectNominalPrf.WPPReplay.gPm201d ph ps (NFChoice.DirectNominalPrf.WPPReplay.gEx ph ps ps.neg hyp_pm2_01da_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm33 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf (((Compiler.CompactSourceSyntax.synWa ph ps).imp ch).imp (ph.imp (ps.imp ch)))

Checked nominal proof certificate identified upstream as g_pm3_3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm331 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf ((ph.imp (ps.imp ch)).imp ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch))

Checked nominal proof certificate identified upstream as g_pm3_31.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm331 ph ps ch = NFChoice.DirectNominalPrf.WPPReplay.gImp3a (ph.imp (ps.imp ch)) ph ps ch (NFChoice.DirectNominalPrf.WPPReplay.gId (ph.imp (ps.imp ch)))

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpexp (ph ps ch : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch) (ph.imp (ps.imp ch)))

Checked nominal proof certificate identified upstream as g_impexp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.g_pm3_2 (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_pm3_2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm321 (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWa ps ph)))

Checked nominal proof certificate identified upstream as g_pm3_21.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm322 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (Compiler.CompactSourceSyntax.synWa ps ph))

Checked nominal proof certificate identified upstream as g_pm3_22.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAncom (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph ps) (Compiler.CompactSourceSyntax.synWa ps ph))

Checked nominal proof certificate identified upstream as g_ancom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAncomd (ph ps ch : SemanticCore.Wff) (hyp_ancomd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ch ps))

Checked nominal proof certificate identified upstream as g_ancomd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAncoms (ph ps ch : SemanticCore.Wff) (hyp_ancoms_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ph).imp ch)

Checked nominal proof certificate identified upstream as g_ancoms.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAncoms ph ps ch hyp_ancoms_1 = NFChoice.DirectNominalPrf.WPPReplay.gImp ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gExpcom ph ps ch hyp_ancoms_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAncomsd (ph ps ch th : SemanticCore.Wff) (hyp_ancomsd_1 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps ch).imp th))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ch ps).imp th))

Checked nominal proof certificate identified upstream as g_ancomsd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm32i (ph ps : SemanticCore.Wff) (hyp_pm3_2i_1 : Nominal.NPrf ph) (hyp_pm3_2i_2 : Nominal.NPrf ps) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWa ph ps)

Checked nominal proof certificate identified upstream as g_pm3_2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm343i (ph ps ch : SemanticCore.Wff) : Nominal.NPrf ((ph.imp ps).imp ((ph.imp ch).imp (ph.imp (Compiler.CompactSourceSyntax.synWa ps ch))))

Checked nominal proof certificate identified upstream as g_pm3_43i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSimpl (ph ps : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ph)

Checked nominal proof certificate identified upstream as g_simpl.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSimpl ph ps = NFChoice.DirectNominalPrf.WPPReplay.gImp ph ps ph (NFChoice.DirectNominalPrf.Nominal.ax1 ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSimpli (ph ps : SemanticCore.Wff) (hyp_simpli_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWa ph ps)) : Nominal.NPrf ph

Checked nominal proof certificate identified upstream as g_simpli.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSimpli ph ps hyp_simpli_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_simpli_1 (NFChoice.DirectNominalPrf.WPPReplay.gSimpl ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSimpld (ph ps ch : SemanticCore.Wff) (hyp_simpld_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ps ch))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_simpld.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSimplbi (ph ps ch : SemanticCore.Wff) (hyp_simplbi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWa ps ch))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_simplbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSimpr (ph ps : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ps)

Checked nominal proof certificate identified upstream as g_simpr.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSimpr ph ps = NFChoice.DirectNominalPrf.WPPReplay.gImp ph ps ps (NFChoice.DirectNominalPrf.WPPReplay.gIdd ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSimpri (ph ps : SemanticCore.Wff) (hyp_simpri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWa ph ps)) : Nominal.NPrf ps

Checked nominal proof certificate identified upstream as g_simpri.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSimpri ph ps hyp_simpri_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_simpri_1 (NFChoice.DirectNominalPrf.WPPReplay.gSimpr ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSimprd (ph ps ch : SemanticCore.Wff) (hyp_simprd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ps ch))) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_simprd.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSimprd ph ps ch hyp_simprd_1 = NFChoice.DirectNominalPrf.WPPReplay.gSimpld ph ch ps (NFChoice.DirectNominalPrf.WPPReplay.gAncomd ph ps ch hyp_simprd_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSimprbi (ph ps ch : SemanticCore.Wff) (hyp_simprbi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWa ps ch))) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_simprbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAdantr (ph ps ch : SemanticCore.Wff) (hyp_adantr_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp ps)

Checked nominal proof certificate identified upstream as g_adantr.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAdantr ph ps ch hyp_adantr_1 = NFChoice.DirectNominalPrf.WPPReplay.gImp ph ch ps (NFChoice.DirectNominalPrf.WPPReplay.gA1d ph ps ch hyp_adantr_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAdantl (ph ps ch : SemanticCore.Wff) (hyp_adantl_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ch ph).imp ps)

Checked nominal proof certificate identified upstream as g_adantl.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAdantl ph ps ch hyp_adantl_1 = NFChoice.DirectNominalPrf.WPPReplay.gAncoms ph ch ps (NFChoice.DirectNominalPrf.WPPReplay.gAdantr ph ps ch hyp_adantl_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAdantld (ph ps ch th : SemanticCore.Wff) (hyp_adantld_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa th ps).imp ch))

Checked nominal proof certificate identified upstream as g_adantld.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAdantrd (ph ps ch th : SemanticCore.Wff) (hyp_adantrd_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps th).imp ch))

Checked nominal proof certificate identified upstream as g_adantrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpan9 (ph ps ch th : SemanticCore.Wff) (hyp_mpan9_1 : Nominal.NPrf (ph.imp ps)) (hyp_mpan9_2 : Nominal.NPrf (ch.imp (ps.imp th))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp th)

Checked nominal proof certificate identified upstream as g_mpan9.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyldan (ph ps ch th : SemanticCore.Wff) (hyp_syldan_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) (hyp_syldan_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp th)

Checked nominal proof certificate identified upstream as g_syldan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan (ph ps ch th : SemanticCore.Wff) (hyp_sylan_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylan_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp th)

Checked nominal proof certificate identified upstream as g_sylan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylanb (ph ps ch th : SemanticCore.Wff) (hyp_sylanb_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_sylanb_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp th)

Checked nominal proof certificate identified upstream as g_sylanb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylanbr (ph ps ch th : SemanticCore.Wff) (hyp_sylanbr_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps ph)) (hyp_sylanbr_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp th)

Checked nominal proof certificate identified upstream as g_sylanbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan2 (ph ps ch th : SemanticCore.Wff) (hyp_sylan2_1 : Nominal.NPrf (ph.imp ch)) (hyp_sylan2_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ph).imp th)

Checked nominal proof certificate identified upstream as g_sylan2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan2b (ph ps ch th : SemanticCore.Wff) (hyp_sylan2b_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ch)) (hyp_sylan2b_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ph).imp th)

Checked nominal proof certificate identified upstream as g_sylan2b.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan2br (ph ps ch th : SemanticCore.Wff) (hyp_sylan2br_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch ph)) (hyp_sylan2br_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ph).imp th)

Checked nominal proof certificate identified upstream as g_sylan2br.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl2an (ph ps ch th ta : SemanticCore.Wff) (hyp_syl2an_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl2an_2 : Nominal.NPrf (ta.imp ch)) (hyp_syl2an_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ta).imp th)

Checked nominal proof certificate identified upstream as g_syl2an.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl2anr (ph ps ch th ta : SemanticCore.Wff) (hyp_syl2an_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl2an_2 : Nominal.NPrf (ta.imp ch)) (hyp_syl2an_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ta ph).imp th)

Checked nominal proof certificate identified upstream as g_syl2anr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl2anb (ph ps ch th ta : SemanticCore.Wff) (hyp_syl2anb_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_syl2anb_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ta ch)) (hyp_syl2anb_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ta).imp th)

Checked nominal proof certificate identified upstream as g_syl2anb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyland (ph ps ch th ta : SemanticCore.Wff) (hyp_syland_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_syland_2 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ch th).imp ta))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps th).imp ta))

Checked nominal proof certificate identified upstream as g_syland.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan2d (ph ps ch th ta : SemanticCore.Wff) (hyp_sylan2d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_sylan2d_2 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa th ch).imp ta))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa th ps).imp ta))

Checked nominal proof certificate identified upstream as g_sylan2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl2and (ph ps ch th ta et : SemanticCore.Wff) (hyp_syl2and_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_syl2and_2 : Nominal.NPrf (ph.imp (th.imp ta))) (hyp_syl2and_3 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ch ta).imp et))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps th).imp et))

Checked nominal proof certificate identified upstream as g_syl2and.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiimpa (ph ps ch : SemanticCore.Wff) (hyp_biimpa_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)

Checked nominal proof certificate identified upstream as g_biimpa.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiimpa ph ps ch hyp_biimpa_1 = NFChoice.DirectNominalPrf.WPPReplay.gImp ph ps ch (NFChoice.DirectNominalPrf.WPPReplay.gBiimpd ph ps ch hyp_biimpa_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiimpar (ph ps ch : SemanticCore.Wff) (hyp_biimpa_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp ps)

Checked nominal proof certificate identified upstream as g_biimpar.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiimpar ph ps ch hyp_biimpa_1 = NFChoice.DirectNominalPrf.WPPReplay.gImp ph ch ps (NFChoice.DirectNominalPrf.WPPReplay.gBiimprd ph ps ch hyp_biimpa_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiimpac (ph ps ch : SemanticCore.Wff) (hyp_biimpa_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ph).imp ch)

Checked nominal proof certificate identified upstream as g_biimpac.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiimpac ph ps ch hyp_biimpa_1 = NFChoice.DirectNominalPrf.WPPReplay.gImp ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gBiimpcd ph ps ch hyp_biimpa_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiimparc (ph ps ch : SemanticCore.Wff) (hyp_biimpa_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ch ph).imp ps)

Checked nominal proof certificate identified upstream as g_biimparc.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiimparc ph ps ch hyp_biimpa_1 = NFChoice.DirectNominalPrf.WPPReplay.gImp ch ph ps (NFChoice.DirectNominalPrf.WPPReplay.gBiimprcd ph ps ch hyp_biimpa_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIanor (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph ps).neg (Compiler.CompactSourceSyntax.synWo ph.neg ps.neg))

Checked nominal proof certificate identified upstream as g_ianor.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIoran (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo ph ps).neg (Compiler.CompactSourceSyntax.synWa ph.neg ps.neg))

Checked nominal proof certificate identified upstream as g_ioran.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm456 (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph.neg ps.neg) (Compiler.CompactSourceSyntax.synWo ph ps).neg)

Checked nominal proof certificate identified upstream as g_pm4_56.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOran (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo ph ps) (Compiler.CompactSourceSyntax.synWa ph.neg ps.neg).neg)

Checked nominal proof certificate identified upstream as g_oran.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIba (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps (Compiler.CompactSourceSyntax.synWa ps ph)))

Checked nominal proof certificate identified upstream as g_iba.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIbar (ph ps : SemanticCore.Wff) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_ibar.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiantru (ph ps : SemanticCore.Wff) (hyp_biantru_1 : Nominal.NPrf ph) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps (Compiler.CompactSourceSyntax.synWa ps ph))

Checked nominal proof certificate identified upstream as g_biantru.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiantru ph ps hyp_biantru_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_biantru_1 (NFChoice.DirectNominalPrf.WPPReplay.gIba ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiantrur (ph ps : SemanticCore.Wff) (hyp_biantrur_1 : Nominal.NPrf ph) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps (Compiler.CompactSourceSyntax.synWa ph ps))

Checked nominal proof certificate identified upstream as g_biantrur.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBiantrur ph ps hyp_biantrur_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_biantrur_1 (NFChoice.DirectNominalPrf.WPPReplay.gIbar ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiantrud (ph ps ch : SemanticCore.Wff) (hyp_biantrud_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch (Compiler.CompactSourceSyntax.synWa ch ps)))

Checked nominal proof certificate identified upstream as g_biantrud.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiantrurd (ph ps ch : SemanticCore.Wff) (hyp_biantrud_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch (Compiler.CompactSourceSyntax.synWa ps ch)))

Checked nominal proof certificate identified upstream as g_biantrurd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJaao (ph ps ch th ta : SemanticCore.Wff) (hyp_jaao_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_jaao_2 : Nominal.NPrf (th.imp (ta.imp ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph th).imp ((Compiler.CompactSourceSyntax.synWo ps ta).imp ch))

Checked nominal proof certificate identified upstream as g_jaao.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm344 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (ps.imp ph) (ch.imp ph)).imp ((Compiler.CompactSourceSyntax.synWo ps ch).imp ph))

Checked nominal proof certificate identified upstream as g_pm3_44.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJao (ph ps ch : SemanticCore.Wff) : Nominal.NPrf ((ph.imp ps).imp ((ch.imp ps).imp ((Compiler.CompactSourceSyntax.synWo ph ch).imp ps)))

Checked nominal proof certificate identified upstream as g_jao.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.g_pm1_2 (ph : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWo ph ph).imp ph)

Checked nominal proof certificate identified upstream as g_pm1_2.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.g_pm1_2 ph = NFChoice.DirectNominalPrf.WPPReplay.gJaoi ph ph ph (NFChoice.DirectNominalPrf.WPPReplay.gId ph) (NFChoice.DirectNominalPrf.WPPReplay.gId ph)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOridm (ph : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo ph ph) ph)

Checked nominal proof certificate identified upstream as g_oridm.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrim12i (ph ps ch th : SemanticCore.Wff) (hyp_orim12i_1 : Nominal.NPrf (ph.imp ps)) (hyp_orim12i_2 : Nominal.NPrf (ch.imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWo ph ch).imp (Compiler.CompactSourceSyntax.synWo ps th))

Checked nominal proof certificate identified upstream as g_orim12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrim2i (ph ps ch : SemanticCore.Wff) (hyp_orim1i_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWo ch ph).imp (Compiler.CompactSourceSyntax.synWo ch ps))

Checked nominal proof certificate identified upstream as g_orim2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gOrim2i ph ps ch hyp_orim1i_1 = NFChoice.DirectNominalPrf.WPPReplay.gOrim12i ch ch ph ps (NFChoice.DirectNominalPrf.WPPReplay.gId ch) hyp_orim1i_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrbi2i (ph ps ch : SemanticCore.Wff) (hyp_orbi2i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo ch ph) (Compiler.CompactSourceSyntax.synWo ch ps))

Checked nominal proof certificate identified upstream as g_orbi2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrbi1i (ph ps ch : SemanticCore.Wff) (hyp_orbi2i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo ph ch) (Compiler.CompactSourceSyntax.synWo ps ch))

Checked nominal proof certificate identified upstream as g_orbi1i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrbi12i (ph ps ch th : SemanticCore.Wff) (hyp_orbi12i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_orbi12i_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo ph ch) (Compiler.CompactSourceSyntax.synWo ps th))

Checked nominal proof certificate identified upstream as g_orbi12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm15 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWo ph (Compiler.CompactSourceSyntax.synWo ps ch)).imp (Compiler.CompactSourceSyntax.synWo ps (Compiler.CompactSourceSyntax.synWo ph ch)))

Checked nominal proof certificate identified upstream as g_pm1_5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOr12 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo ph (Compiler.CompactSourceSyntax.synWo ps ch)) (Compiler.CompactSourceSyntax.synWo ps (Compiler.CompactSourceSyntax.synWo ph ch)))

Checked nominal proof certificate identified upstream as g_or12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrass (ph ps ch : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWo ph ps) ch) (Compiler.CompactSourceSyntax.synWo ph (Compiler.CompactSourceSyntax.synWo ps ch)))

Checked nominal proof certificate identified upstream as g_orass.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOr32 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWo ph ps) ch) (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWo ph ch) ps))

Checked nominal proof certificate identified upstream as g_or32.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJca (ph ps ch : SemanticCore.Wff) (hyp_jca_1 : Nominal.NPrf (ph.imp ps)) (hyp_jca_2 : Nominal.NPrf (ph.imp ch)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ps ch))

Checked nominal proof certificate identified upstream as g_jca.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJcad (ph ps ch th : SemanticCore.Wff) (hyp_jcad_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_jcad_2 : Nominal.NPrf (ph.imp (ps.imp th))) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWa ch th)))

Checked nominal proof certificate identified upstream as g_jcad.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJca31 (ph ps ch th : SemanticCore.Wff) (hyp_jca31_1 : Nominal.NPrf (ph.imp ps)) (hyp_jca31_2 : Nominal.NPrf (ph.imp ch)) (hyp_jca31_3 : Nominal.NPrf (ph.imp th)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ps ch) th))

Checked nominal proof certificate identified upstream as g_jca31.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJca32 (ph ps ch th : SemanticCore.Wff) (hyp_jca31_1 : Nominal.NPrf (ph.imp ps)) (hyp_jca31_2 : Nominal.NPrf (ph.imp ch)) (hyp_jca31_3 : Nominal.NPrf (ph.imp th)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ps (Compiler.CompactSourceSyntax.synWa ch th)))

Checked nominal proof certificate identified upstream as g_jca32.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJcai (ph ps ch : SemanticCore.Wff) (hyp_jcai_1 : Nominal.NPrf (ph.imp ps)) (hyp_jcai_2 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ps ch))

Checked nominal proof certificate identified upstream as g_jcai.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJctil (ph ps ch : SemanticCore.Wff) (hyp_jctil_1 : Nominal.NPrf (ph.imp ps)) (hyp_jctil_2 : Nominal.NPrf ch) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ch ps))

Checked nominal proof certificate identified upstream as g_jctil.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJctir (ph ps ch : SemanticCore.Wff) (hyp_jctil_1 : Nominal.NPrf (ph.imp ps)) (hyp_jctil_2 : Nominal.NPrf ch) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ps ch))

Checked nominal proof certificate identified upstream as g_jctir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJctl (ph ps : SemanticCore.Wff) (hyp_jctl_1 : Nominal.NPrf ps) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ps ph))

Checked nominal proof certificate identified upstream as g_jctl.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gJctl ph ps hyp_jctl_1 = NFChoice.DirectNominalPrf.WPPReplay.gJctil ph ph ps (NFChoice.DirectNominalPrf.WPPReplay.gId ph) hyp_jctl_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJctr (ph ps : SemanticCore.Wff) (hyp_jctl_1 : Nominal.NPrf ps) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ph ps))

Checked nominal proof certificate identified upstream as g_jctr.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gJctr ph ps hyp_jctl_1 = NFChoice.DirectNominalPrf.WPPReplay.gJctir ph ph ps (NFChoice.DirectNominalPrf.WPPReplay.gId ph) hyp_jctl_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJctild (ph ps ch th : SemanticCore.Wff) (hyp_jctild_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_jctild_2 : Nominal.NPrf (ph.imp th)) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWa th ch)))

Checked nominal proof certificate identified upstream as g_jctild.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gJctird (ph ps ch th : SemanticCore.Wff) (hyp_jctird_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_jctird_2 : Nominal.NPrf (ph.imp th)) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWa ch th)))

Checked nominal proof certificate identified upstream as g_jctird.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAncl (ph ps : SemanticCore.Wff) : Nominal.NPrf ((ph.imp ps).imp (ph.imp (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_ancl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnclb (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps) (ph.imp (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_anclb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAncli (ph ps : SemanticCore.Wff) (hyp_ancli_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ph ps))

Checked nominal proof certificate identified upstream as g_ancli.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAncli ph ps hyp_ancli_1 = NFChoice.DirectNominalPrf.WPPReplay.gJca ph ph ps (NFChoice.DirectNominalPrf.WPPReplay.gId ph) hyp_ancli_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAncri (ph ps : SemanticCore.Wff) (hyp_ancri_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa ps ph))

Checked nominal proof certificate identified upstream as g_ancri.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAncri ph ps hyp_ancri_1 = NFChoice.DirectNominalPrf.WPPReplay.gJca ph ps ph hyp_ancri_1 (NFChoice.DirectNominalPrf.WPPReplay.gId ph)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAncld (ph ps ch : SemanticCore.Wff) (hyp_ancld_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWa ps ch)))

Checked nominal proof certificate identified upstream as g_ancld.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAncld ph ps ch hyp_ancld_1 = NFChoice.DirectNominalPrf.WPPReplay.gJcad ph ps ps ch (NFChoice.DirectNominalPrf.WPPReplay.gIdd ph ps) hyp_ancld_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAncrd (ph ps ch : SemanticCore.Wff) (hyp_ancrd_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWa ch ps)))

Checked nominal proof certificate identified upstream as g_ancrd.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAncrd ph ps ch hyp_ancrd_1 = NFChoice.DirectNominalPrf.WPPReplay.gJcad ph ps ch ps hyp_ancrd_1 (NFChoice.DirectNominalPrf.WPPReplay.gIdd ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnc2li (ph ps ch : SemanticCore.Wff) (hyp_anc2li_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWa ph ch)))

Checked nominal proof certificate identified upstream as g_anc2li.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAnc2li ph ps ch hyp_anc2li_1 = NFChoice.DirectNominalPrf.WPPReplay.gJctild ph ps ch ph hyp_anc2li_1 (NFChoice.DirectNominalPrf.WPPReplay.gId ph)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnc2ri (ph ps ch : SemanticCore.Wff) (hyp_anc2ri_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWa ch ph)))

Checked nominal proof certificate identified upstream as g_anc2ri.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAnc2ri ph ps ch hyp_anc2ri_1 = NFChoice.DirectNominalPrf.WPPReplay.gJctird ph ps ch ph hyp_anc2ri_1 (NFChoice.DirectNominalPrf.WPPReplay.gId ph)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm34 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (ph.imp ps))

Checked nominal proof certificate identified upstream as g_pm3_4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm445im (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWa ph (ps.imp ph)))

Checked nominal proof certificate identified upstream as g_pm4_45im.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnim12d (ph ps ch th ta : SemanticCore.Wff) (hyp_anim12d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_anim12d_2 : Nominal.NPrf (ph.imp (th.imp ta))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps th).imp (Compiler.CompactSourceSyntax.synWa ch ta)))

Checked nominal proof certificate identified upstream as g_anim12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnim1d (ph ps ch th : SemanticCore.Wff) (hyp_anim1d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps th).imp (Compiler.CompactSourceSyntax.synWa ch th)))

Checked nominal proof certificate identified upstream as g_anim1d.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAnim1d ph ps ch th hyp_anim1d_1 = NFChoice.DirectNominalPrf.WPPReplay.gAnim12d ph ps ch th th hyp_anim1d_1 (NFChoice.DirectNominalPrf.WPPReplay.gIdd ph th)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnim2d (ph ps ch th : SemanticCore.Wff) (hyp_anim1d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa th ps).imp (Compiler.CompactSourceSyntax.synWa th ch)))

Checked nominal proof certificate identified upstream as g_anim2d.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAnim2d ph ps ch th hyp_anim1d_1 = NFChoice.DirectNominalPrf.WPPReplay.gAnim12d ph th th ps ch (NFChoice.DirectNominalPrf.WPPReplay.gIdd ph th) hyp_anim1d_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnim12i (ph ps ch th : SemanticCore.Wff) (hyp_anim12i_1 : Nominal.NPrf (ph.imp ps)) (hyp_anim12i_2 : Nominal.NPrf (ch.imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp (Compiler.CompactSourceSyntax.synWa ps th))

Checked nominal proof certificate identified upstream as g_anim12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnim12ci (ph ps ch th : SemanticCore.Wff) (hyp_anim12i_1 : Nominal.NPrf (ph.imp ps)) (hyp_anim12i_2 : Nominal.NPrf (ch.imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp (Compiler.CompactSourceSyntax.synWa th ps))

Checked nominal proof certificate identified upstream as g_anim12ci.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnim1i (ph ps ch : SemanticCore.Wff) (hyp_anim1i_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp (Compiler.CompactSourceSyntax.synWa ps ch))

Checked nominal proof certificate identified upstream as g_anim1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAnim1i ph ps ch hyp_anim1i_1 = NFChoice.DirectNominalPrf.WPPReplay.gAnim12i ph ps ch ch hyp_anim1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gId ch)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnim2i (ph ps ch : SemanticCore.Wff) (hyp_anim1i_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ch ph).imp (Compiler.CompactSourceSyntax.synWa ch ps))

Checked nominal proof certificate identified upstream as g_anim2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAnim2i ph ps ch hyp_anim1i_1 = NFChoice.DirectNominalPrf.WPPReplay.gAnim12i ch ch ph ps (NFChoice.DirectNominalPrf.WPPReplay.gId ch) hyp_anim1i_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnim12ii (ph ps ch th ta : SemanticCore.Wff) (hyp_anim12ii_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_anim12ii_2 : Nominal.NPrf (th.imp (ps.imp ta))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph th).imp (ps.imp (Compiler.CompactSourceSyntax.synWa ch ta)))

Checked nominal proof certificate identified upstream as g_anim12ii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPrth (ph ps ch th : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (ph.imp ps) (ch.imp th)).imp ((Compiler.CompactSourceSyntax.synWa ph ch).imp (Compiler.CompactSourceSyntax.synWa ps th)))

Checked nominal proof certificate identified upstream as g_prth.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm335 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (ph.imp ps)).imp ps)

Checked nominal proof certificate identified upstream as g_pm3_35.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm335 ph ps = NFChoice.DirectNominalPrf.WPPReplay.gImp ph (ph.imp ps) ps (NFChoice.DirectNominalPrf.WPPReplay.gPm227 ph ps)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImp4a (ph ps ch th ta : SemanticCore.Wff) (hyp_imp4_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))) : Nominal.NPrf (ph.imp (ps.imp ((Compiler.CompactSourceSyntax.synWa ch th).imp ta)))

Checked nominal proof certificate identified upstream as g_imp4a.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImp4c (ph ps ch th ta : SemanticCore.Wff) (hyp_imp4_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ps ch) th).imp ta))

Checked nominal proof certificate identified upstream as g_imp4c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExpimpd (ph ps ch th : SemanticCore.Wff) (hyp_expimpd_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (ch.imp th))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps ch).imp th))

Checked nominal proof certificate identified upstream as g_expimpd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExp31 (ph ps ch th : SemanticCore.Wff) (hyp_exp31_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) ch).imp th)) : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))

Checked nominal proof certificate identified upstream as g_exp31.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExp32 (ph ps ch th : SemanticCore.Wff) (hyp_exp32_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ch)).imp th)) : Nominal.NPrf (ph.imp (ps.imp (ch.imp th)))

Checked nominal proof certificate identified upstream as g_exp32.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExp4a (ph ps ch th ta : SemanticCore.Wff) (hyp_exp4a_1 : Nominal.NPrf (ph.imp (ps.imp ((Compiler.CompactSourceSyntax.synWa ch th).imp ta)))) : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))

Checked nominal proof certificate identified upstream as g_exp4a.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExp4b (ph ps ch th ta : SemanticCore.Wff) (hyp_exp4b_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ((Compiler.CompactSourceSyntax.synWa ch th).imp ta))) : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))

Checked nominal proof certificate identified upstream as g_exp4b.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExp4d (ph ps ch th ta : SemanticCore.Wff) (hyp_exp4d_1 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps (Compiler.CompactSourceSyntax.synWa ch th)).imp ta))) : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))

Checked nominal proof certificate identified upstream as g_exp4d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExp42 (ph ps ch th ta : SemanticCore.Wff) (hyp_exp42_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ch)) th).imp ta)) : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))

Checked nominal proof certificate identified upstream as g_exp42.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExp43 (ph ps ch th ta : SemanticCore.Wff) (hyp_exp43_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) (Compiler.CompactSourceSyntax.synWa ch th)).imp ta)) : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))

Checked nominal proof certificate identified upstream as g_exp43.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExp45 (ph ps ch th ta : SemanticCore.Wff) (hyp_exp45_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps (Compiler.CompactSourceSyntax.synWa ch th))).imp ta)) : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))

Checked nominal proof certificate identified upstream as g_exp45.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExpr (ph ps ch th : SemanticCore.Wff) (hyp_expr_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ch)).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (ch.imp th))

Checked nominal proof certificate identified upstream as g_expr.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gExpr ph ps ch th hyp_expr_1 = NFChoice.DirectNominalPrf.WPPReplay.gImp ph ps (ch.imp th) (NFChoice.DirectNominalPrf.WPPReplay.gExp32 ph ps ch th hyp_expr_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gExp5c (ph ps ch th ta et : SemanticCore.Wff) (hyp_exp5c_1 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps ch).imp ((Compiler.CompactSourceSyntax.synWa th ta).imp et)))) : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp (ta.imp et)))))

Checked nominal proof certificate identified upstream as g_exp5c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpr (ph ps ch th : SemanticCore.Wff) (hyp_impr_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (ch.imp th))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ch)).imp th)

Checked nominal proof certificate identified upstream as g_impr.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gImpr ph ps ch th hyp_impr_1 = NFChoice.DirectNominalPrf.WPPReplay.gImp32 ph ps ch th (NFChoice.DirectNominalPrf.WPPReplay.gEx ph ps (ch.imp th) hyp_impr_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImpac (ph ps ch : SemanticCore.Wff) (hyp_impac_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (Compiler.CompactSourceSyntax.synWa ch ps))

Checked nominal proof certificate identified upstream as g_impac.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSimprbda (ph ps ch th : SemanticCore.Wff) (hyp_pm3_26bda_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps (Compiler.CompactSourceSyntax.synWa ch th)))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)

Checked nominal proof certificate identified upstream as g_simprbda.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSimplbi2 (ph ps ch : SemanticCore.Wff) (hyp_pm3_26bi2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWa ps ch))) : Nominal.NPrf (ps.imp (ch.imp ph))

Checked nominal proof certificate identified upstream as g_simplbi2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfbi2 (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWb ph ps) (Compiler.CompactSourceSyntax.synWa (ph.imp ps) (ps.imp ph)))

Checked nominal proof certificate identified upstream as g_dfbi2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm471 (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps) (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_pm4_71.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm471r (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp ps) (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWa ps ph)))

Checked nominal proof certificate identified upstream as g_pm4_71r.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm471i (ph ps : SemanticCore.Wff) (hyp_pm4_71i_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWa ph ps))

Checked nominal proof certificate identified upstream as g_pm4_71i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm471ri (ph ps : SemanticCore.Wff) (hyp_pm4_71ri_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWa ps ph))

Checked nominal proof certificate identified upstream as g_pm4_71ri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm471rd (ph ps ch : SemanticCore.Wff) (hyp_pm4_71rd_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps (Compiler.CompactSourceSyntax.synWa ch ps)))

Checked nominal proof certificate identified upstream as g_pm4_71rd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm532 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch)) (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph ps) (Compiler.CompactSourceSyntax.synWa ph ch)))

Checked nominal proof certificate identified upstream as g_pm5_32.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm532i (ph ps ch : SemanticCore.Wff) (hyp_pm5_32i_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph ps) (Compiler.CompactSourceSyntax.synWa ph ch))

Checked nominal proof certificate identified upstream as g_pm5_32i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm532ri (ph ps ch : SemanticCore.Wff) (hyp_pm5_32i_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ps ph) (Compiler.CompactSourceSyntax.synWa ch ph))

Checked nominal proof certificate identified upstream as g_pm5_32ri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm532d (ph ps ch th : SemanticCore.Wff) (hyp_pm5_32d_1 : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWb ch th)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ps ch) (Compiler.CompactSourceSyntax.synWa ps th)))

Checked nominal proof certificate identified upstream as g_pm5_32d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm532rd (ph ps ch th : SemanticCore.Wff) (hyp_pm5_32d_1 : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synWb ch th)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ch ps) (Compiler.CompactSourceSyntax.synWa th ps)))

Checked nominal proof certificate identified upstream as g_pm5_32rd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm532da (ph ps ch th : SemanticCore.Wff) (hyp_pm5_32da_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (Compiler.CompactSourceSyntax.synWb ch th))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ps ch) (Compiler.CompactSourceSyntax.synWa ps th)))

Checked nominal proof certificate identified upstream as g_pm5_32da.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBiadan2 (ph ps ch : SemanticCore.Wff) (hyp_biadan2_1 : Nominal.NPrf (ph.imp ps)) (hyp_biadan2_2 : Nominal.NPrf (ps.imp (Compiler.CompactSourceSyntax.synWb ph ch))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWa ps ch))

Checked nominal proof certificate identified upstream as g_biadan2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm424 (ph : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWa ph ph))

Checked nominal proof certificate identified upstream as g_pm4_24.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPm424 ph = NFChoice.DirectNominalPrf.WPPReplay.gPm471i ph ph (NFChoice.DirectNominalPrf.WPPReplay.gId ph)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnidm (ph : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph ph) ph)

Checked nominal proof certificate identified upstream as g_anidm.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnidms (ph ps : SemanticCore.Wff) (hyp_anidms_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ph).imp ps)) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_anidms.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAnidms ph ps hyp_anidms_1 = NFChoice.DirectNominalPrf.WPPReplay.gPm243i ph ps (NFChoice.DirectNominalPrf.WPPReplay.gEx ph ph ps hyp_anidms_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnasss (ph ps ch th : SemanticCore.Wff) (hyp_anasss_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ch)).imp th)

Checked nominal proof certificate identified upstream as g_anasss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnassrs (ph ps ch th : SemanticCore.Wff) (hyp_anassrs_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ch)).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) ch).imp th)

Checked nominal proof certificate identified upstream as g_anassrs.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnass (ph ps ch : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) ch) (Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ch)))

Checked nominal proof certificate identified upstream as g_anass.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylanl1 (ph ps ch th ta : SemanticCore.Wff) (hyp_sylanl1_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylanl1_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ps ch) th).imp ta)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ch) th).imp ta)

Checked nominal proof certificate identified upstream as g_sylanl1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylanl2 (ph ps ch th ta : SemanticCore.Wff) (hyp_sylanl2_1 : Nominal.NPrf (ph.imp ch)) (hyp_sylanl2_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ps ch) th).imp ta)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ps ph) th).imp ta)

Checked nominal proof certificate identified upstream as g_sylanl2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan2i (ph ps ch th ta : SemanticCore.Wff) (hyp_sylan2i_1 : Nominal.NPrf (ph.imp th)) (hyp_sylan2i_2 : Nominal.NPrf (ps.imp ((Compiler.CompactSourceSyntax.synWa ch th).imp ta))) : Nominal.NPrf (ps.imp ((Compiler.CompactSourceSyntax.synWa ch ph).imp ta))

Checked nominal proof certificate identified upstream as g_sylan2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan9 (ph ps ch th ta : SemanticCore.Wff) (hyp_sylan9_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_sylan9_2 : Nominal.NPrf (th.imp (ch.imp ta))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph th).imp (ps.imp ta))

Checked nominal proof certificate identified upstream as g_sylan9.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan9r (ph ps ch th ta : SemanticCore.Wff) (hyp_sylan9r_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_sylan9r_2 : Nominal.NPrf (th.imp (ch.imp ta))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa th ph).imp (ps.imp ta))

Checked nominal proof certificate identified upstream as g_sylan9r.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMtand (ph ps ch : SemanticCore.Wff) (hyp_mtand_1 : Nominal.NPrf (ph.imp ch.neg)) (hyp_mtand_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf (ph.imp ps.neg)

Checked nominal proof certificate identified upstream as g_mtand.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl2anc (ph ps ch th : SemanticCore.Wff) (hyp_syl2anc_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl2anc_2 : Nominal.NPrf (ph.imp ch)) (hyp_syl2anc_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)) : Nominal.NPrf (ph.imp th)

Checked nominal proof certificate identified upstream as g_syl2anc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylancl (ph ps ch th : SemanticCore.Wff) (hyp_sylancl_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylancl_2 : Nominal.NPrf ch) (hyp_sylancl_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)) : Nominal.NPrf (ph.imp th)

Checked nominal proof certificate identified upstream as g_sylancl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylancr (ph ps ch th : SemanticCore.Wff) (hyp_sylancr_1 : Nominal.NPrf ps) (hyp_sylancr_2 : Nominal.NPrf (ph.imp ch)) (hyp_sylancr_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)) : Nominal.NPrf (ph.imp th)

Checked nominal proof certificate identified upstream as g_sylancr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylanbrc (ph ps ch th : SemanticCore.Wff) (hyp_sylanbrc_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylanbrc_2 : Nominal.NPrf (ph.imp ch)) (hyp_sylanbrc_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb th (Compiler.CompactSourceSyntax.synWa ps ch))) : Nominal.NPrf (ph.imp th)

Checked nominal proof certificate identified upstream as g_sylanbrc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpdan (ph ps ch : SemanticCore.Wff) (hyp_mpdan_1 : Nominal.NPrf (ph.imp ps)) (hyp_mpdan_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_mpdan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpancom (ph ps ch : SemanticCore.Wff) (hyp_mpancom_1 : Nominal.NPrf (ps.imp ph)) (hyp_mpancom_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf (ps.imp ch)

Checked nominal proof certificate identified upstream as g_mpancom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpan (ph ps ch : SemanticCore.Wff) (hyp_mpan_1 : Nominal.NPrf ph) (hyp_mpan_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf (ps.imp ch)

Checked nominal proof certificate identified upstream as g_mpan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpan2 (ph ps ch : SemanticCore.Wff) (hyp_mpan2_1 : Nominal.NPrf ps) (hyp_mpan2_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf (ph.imp ch)

Checked nominal proof certificate identified upstream as g_mpan2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMp2an (ph ps ch : SemanticCore.Wff) (hyp_mp2an_1 : Nominal.NPrf ph) (hyp_mp2an_2 : Nominal.NPrf ps) (hyp_mp2an_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf ch

Checked nominal proof certificate identified upstream as g_mp2an.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMp4an (ph ps ch th ta : SemanticCore.Wff) (hyp_mp4an_1 : Nominal.NPrf ph) (hyp_mp4an_2 : Nominal.NPrf ps) (hyp_mp4an_3 : Nominal.NPrf ch) (hyp_mp4an_4 : Nominal.NPrf th) (hyp_mp4an_5 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) (Compiler.CompactSourceSyntax.synWa ch th)).imp ta)) : Nominal.NPrf ta

Checked nominal proof certificate identified upstream as g_mp4an.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpan2d (ph ps ch th : SemanticCore.Wff) (hyp_mpan2d_1 : Nominal.NPrf (ph.imp ch)) (hyp_mpan2d_2 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps ch).imp th))) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_mpan2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpand (ph ps ch th : SemanticCore.Wff) (hyp_mpand_1 : Nominal.NPrf (ph.imp ps)) (hyp_mpand_2 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps ch).imp th))) : Nominal.NPrf (ph.imp (ch.imp th))

Checked nominal proof certificate identified upstream as g_mpand.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpani (ph ps ch th : SemanticCore.Wff) (hyp_mpani_1 : Nominal.NPrf ps) (hyp_mpani_2 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps ch).imp th))) : Nominal.NPrf (ph.imp (ch.imp th))

Checked nominal proof certificate identified upstream as g_mpani.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpan2i (ph ps ch th : SemanticCore.Wff) (hyp_mpan2i_1 : Nominal.NPrf ch) (hyp_mpan2i_2 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps ch).imp th))) : Nominal.NPrf (ph.imp (ps.imp th))

Checked nominal proof certificate identified upstream as g_mpan2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMp2ani (ph ps ch th : SemanticCore.Wff) (hyp_mp2ani_1 : Nominal.NPrf ps) (hyp_mp2ani_2 : Nominal.NPrf ch) (hyp_mp2ani_3 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps ch).imp th))) : Nominal.NPrf (ph.imp th)

Checked nominal proof certificate identified upstream as g_mp2ani.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMp2and (ph ps ch th : SemanticCore.Wff) (hyp_mp2and_1 : Nominal.NPrf (ph.imp ps)) (hyp_mp2and_2 : Nominal.NPrf (ph.imp ch)) (hyp_mp2and_3 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWa ps ch).imp th))) : Nominal.NPrf (ph.imp th)

Checked nominal proof certificate identified upstream as g_mp2and.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpanl1 (ph ps ch th : SemanticCore.Wff) (hyp_mpanl1_1 : Nominal.NPrf ph) (hyp_mpanl1_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)

Checked nominal proof certificate identified upstream as g_mpanl1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpanl2 (ph ps ch th : SemanticCore.Wff) (hyp_mpanl2_1 : Nominal.NPrf ps) (hyp_mpanl2_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp th)

Checked nominal proof certificate identified upstream as g_mpanl2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpanl12 (ph ps ch th : SemanticCore.Wff) (hyp_mpanl12_1 : Nominal.NPrf ph) (hyp_mpanl12_2 : Nominal.NPrf ps) (hyp_mpanl12_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) ch).imp th)) : Nominal.NPrf (ch.imp th)

Checked nominal proof certificate identified upstream as g_mpanl12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpanr1 (ph ps ch th : SemanticCore.Wff) (hyp_mpanr1_1 : Nominal.NPrf ps) (hyp_mpanr1_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ch)).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp th)

Checked nominal proof certificate identified upstream as g_mpanr1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpanr2 (ph ps ch th : SemanticCore.Wff) (hyp_mpanr2_1 : Nominal.NPrf ch) (hyp_mpanr2_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ch)).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp th)

Checked nominal proof certificate identified upstream as g_mpanr2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpanr12 (ph ps ch th : SemanticCore.Wff) (hyp_mpanr12_1 : Nominal.NPrf ps) (hyp_mpanr12_2 : Nominal.NPrf ch) (hyp_mpanr12_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ch)).imp th)) : Nominal.NPrf (ph.imp th)

Checked nominal proof certificate identified upstream as g_mpanr12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm574da (ph ps ch th : SemanticCore.Wff) (hyp_pm5_74da_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (Compiler.CompactSourceSyntax.synWb ch th))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (ps.imp ch) (ps.imp th)))

Checked nominal proof certificate identified upstream as g_pm5_74da.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImdistani (ph ps ch : SemanticCore.Wff) (hyp_imdistani_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (Compiler.CompactSourceSyntax.synWa ph ch))

Checked nominal proof certificate identified upstream as g_imdistani.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnbi2i (ph ps ch : SemanticCore.Wff) (hyp_bi_aa : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ch ph) (Compiler.CompactSourceSyntax.synWa ch ps))

Checked nominal proof certificate identified upstream as g_anbi2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnbi1i (ph ps ch : SemanticCore.Wff) (hyp_bi_aa : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph ch) (Compiler.CompactSourceSyntax.synWa ps ch))

Checked nominal proof certificate identified upstream as g_anbi1i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnbi2ci (ph ps ch : SemanticCore.Wff) (hyp_bi_aa : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph ch) (Compiler.CompactSourceSyntax.synWa ch ps))

Checked nominal proof certificate identified upstream as g_anbi2ci.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnbi12i (ph ps ch th : SemanticCore.Wff) (hyp_anbi12_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_anbi12_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph ch) (Compiler.CompactSourceSyntax.synWa ps th))

Checked nominal proof certificate identified upstream as g_anbi12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnbi12ci (ph ps ch th : SemanticCore.Wff) (hyp_anbi12_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_anbi12_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph ch) (Compiler.CompactSourceSyntax.synWa th ps))

Checked nominal proof certificate identified upstream as g_anbi12ci.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan9bb (ph ps ch th ta : SemanticCore.Wff) (hyp_sylan9bb_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_sylan9bb_2 : Nominal.NPrf (th.imp (Compiler.CompactSourceSyntax.synWb ch ta))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph th).imp (Compiler.CompactSourceSyntax.synWb ps ta))

Checked nominal proof certificate identified upstream as g_sylan9bb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan9bbr (ph ps ch th ta : SemanticCore.Wff) (hyp_sylan9bbr_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_sylan9bbr_2 : Nominal.NPrf (th.imp (Compiler.CompactSourceSyntax.synWb ch ta))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa th ph).imp (Compiler.CompactSourceSyntax.synWb ps ta))

Checked nominal proof certificate identified upstream as g_sylan9bbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrbi2d (ph ps ch th : SemanticCore.Wff) (hyp_bid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo th ps) (Compiler.CompactSourceSyntax.synWo th ch)))

Checked nominal proof certificate identified upstream as g_orbi2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrbi1d (ph ps ch th : SemanticCore.Wff) (hyp_bid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo ps th) (Compiler.CompactSourceSyntax.synWo ch th)))

Checked nominal proof certificate identified upstream as g_orbi1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnbi2d (ph ps ch th : SemanticCore.Wff) (hyp_bid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa th ps) (Compiler.CompactSourceSyntax.synWa th ch)))

Checked nominal proof certificate identified upstream as g_anbi2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnbi1d (ph ps ch th : SemanticCore.Wff) (hyp_bid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ps th) (Compiler.CompactSourceSyntax.synWa ch th)))

Checked nominal proof certificate identified upstream as g_anbi1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnbi1 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb ph ps).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ph ch) (Compiler.CompactSourceSyntax.synWa ps ch)))

Checked nominal proof certificate identified upstream as g_anbi1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrbi12d (ph ps ch th ta : SemanticCore.Wff) (hyp_bi12d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_bi12d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo ps th) (Compiler.CompactSourceSyntax.synWo ch ta)))

Checked nominal proof certificate identified upstream as g_orbi12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAnbi12d (ph ps ch th ta : SemanticCore.Wff) (hyp_bi12d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_bi12d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ps th) (Compiler.CompactSourceSyntax.synWa ch ta)))

Checked nominal proof certificate identified upstream as g_anbi12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm561 (ph ps : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWo ph ps) ps.neg) (Compiler.CompactSourceSyntax.synWa ph ps.neg))

Checked nominal proof certificate identified upstream as g_pm5_61.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAdantll (ph ps ch th : SemanticCore.Wff) (hyp_adant2_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa th ph) ps).imp ch)

Checked nominal proof certificate identified upstream as g_adantll.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAdantlr (ph ps ch th : SemanticCore.Wff) (hyp_adant2_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph th) ps).imp ch)

Checked nominal proof certificate identified upstream as g_adantlr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAdantrl (ph ps ch th : SemanticCore.Wff) (hyp_adant2_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa th ps)).imp ch)

Checked nominal proof certificate identified upstream as g_adantrl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAdantrr (ph ps ch th : SemanticCore.Wff) (hyp_adant2_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps th)).imp ch)

Checked nominal proof certificate identified upstream as g_adantrr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAdantllr (ph ps ch th ta : SemanticCore.Wff) (hyp_adantl2_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ta) ps) ch).imp th)

Checked nominal proof certificate identified upstream as g_adantllr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAdantlrr (ph ps ch th ta : SemanticCore.Wff) (hyp_adantl2_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) ch).imp th)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ta)) ch).imp th)

Checked nominal proof certificate identified upstream as g_adantlrr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAd2antrr (ph ps ch th : SemanticCore.Wff) (hyp_ad2ant_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ch) th).imp ps)

Checked nominal proof certificate identified upstream as g_ad2antrr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAd2antlr (ph ps ch th : SemanticCore.Wff) (hyp_ad2ant_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ch ph) th).imp ps)

Checked nominal proof certificate identified upstream as g_ad2antlr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAd2antrl (ph ps ch th : SemanticCore.Wff) (hyp_ad2ant_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ch (Compiler.CompactSourceSyntax.synWa ph th)).imp ps)

Checked nominal proof certificate identified upstream as g_ad2antrl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAd2antll (ph ps ch th : SemanticCore.Wff) (hyp_ad2ant_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ch (Compiler.CompactSourceSyntax.synWa th ph)).imp ps)

Checked nominal proof certificate identified upstream as g_ad2antll.

Equations

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