NF weak partition development: NominalWPPReplayChunk003.

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

Checked nominal proof certificate identified upstream as g_ad3antrrr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ad2ant2l.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ad2ant2r.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ad2ant2rl.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpll.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSimpll ph ps ch = NFChoice.DirectNominalPrf.WPPReplay.gAd2antrr ph ph ps ch (NFChoice.DirectNominalPrf.WPPReplay.gId ph)

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

Checked nominal proof certificate identified upstream as g_simplr.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSimplr ph ps ch = NFChoice.DirectNominalPrf.WPPReplay.gAd2antlr ps ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gId ps)

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

Checked nominal proof certificate identified upstream as g_simprl.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSimprl ph ps ch = NFChoice.DirectNominalPrf.WPPReplay.gAd2antrl ps ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gId ps)

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

Checked nominal proof certificate identified upstream as g_simprr.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSimprr ph ps ch = NFChoice.DirectNominalPrf.WPPReplay.gAd2antll ch ch ph ps (NFChoice.DirectNominalPrf.WPPReplay.gId ch)

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

Checked nominal proof certificate identified upstream as g_simplll.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpllr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simplrl.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simplrr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simprll.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simprlr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simprrl.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simprrr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_jaob.

Equations

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

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

Checked nominal proof certificate identified upstream as g_jaoian.

Equations

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

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

Checked nominal proof certificate identified upstream as g_jaodan.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pm2_61ian.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pm2_61dan.

Equations

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

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

Checked nominal proof certificate identified upstream as g_abai.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAbai ph ps = NFChoice.DirectNominalPrf.WPPReplay.gPm532i ph ps (ph.imp ps) (NFChoice.DirectNominalPrf.WPPReplay.gBiimt ph ps)

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

Checked nominal proof certificate identified upstream as g_an12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_an32.

Equations

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

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

Checked nominal proof certificate identified upstream as g_an13.

Equations

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

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

Checked nominal proof certificate identified upstream as g_an12s.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ancom2s.

Equations

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

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

Checked nominal proof certificate identified upstream as g_an32s.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anabsan.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anabss1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anabss4.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAnabss4 ph ps ch hyp_anabss4_1 = NFChoice.DirectNominalPrf.WPPReplay.gAncoms ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gAnabss1 ps ph ch hyp_anabss4_1)

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

Checked nominal proof certificate identified upstream as g_anabss5.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anabsi5.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anabsi6.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anabsi7.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAnabsi7 ph ps ch hyp_anabsi7_1 = NFChoice.DirectNominalPrf.WPPReplay.gAncoms ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gAnabsi6 ps ph ch hyp_anabsi7_1)

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

Checked nominal proof certificate identified upstream as g_anabss7.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anabsan2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anabss3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_an4.

Equations

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

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

Checked nominal proof certificate identified upstream as g_an42.

Equations

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

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

Checked nominal proof certificate identified upstream as g_an4s.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anandi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anandir.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anandis.

Equations

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

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

Checked nominal proof certificate identified upstream as g_impbida.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pm3_48.

Equations

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

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

Checked nominal proof certificate identified upstream as g_im2anan9.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anim12dan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOrim12d (ph ps ch th ta : SemanticCore.Wff) (hyp_orim12d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_orim12d_2 : Nominal.NPrf (ph.imp (th.imp ta))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synWo ps th).imp (Compiler.CompactSourceSyntax.synWo ch ta)))

Checked nominal proof certificate identified upstream as g_orim12d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_orim1d.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gOrim1d ph ps ch th hyp_orim1d_1 = NFChoice.DirectNominalPrf.WPPReplay.gOrim12d ph ps ch th th hyp_orim1d_1 (NFChoice.DirectNominalPrf.WPPReplay.gIdd ph th)

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

Checked nominal proof certificate identified upstream as g_pm3_43.

Equations

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

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

Checked nominal proof certificate identified upstream as g_jcab.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ordi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_andi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_andir.

Equations

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

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

Checked nominal proof certificate identified upstream as g_anddi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBi2anan9 (ph ps ch th ta et : SemanticCore.Wff) (hyp_bi2an9_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_bi2an9_2 : Nominal.NPrf (th.imp (Compiler.CompactSourceSyntax.synWb ta et))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph th).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa ps ta) (Compiler.CompactSourceSyntax.synWa ch et)))

Checked nominal proof certificate identified upstream as g_bi2anan9.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pm4_72.

Equations

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

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

Checked nominal proof certificate identified upstream as g_bianabs.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pm3_24.

Equations

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

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

Checked nominal proof certificate identified upstream as g_xor.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dfbi3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_xordi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPm521nd (ph ps ch th : SemanticCore.Wff) (hyp_pm5_21nd_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp th)) (hyp_pm5_21nd_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ch).imp th)) (hyp_pm5_21nd_3 : Nominal.NPrf (th.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))

Checked nominal proof certificate identified upstream as g_pm5_21nd.

Equations

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

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

Checked nominal proof certificate identified upstream as g_baib.

Equations

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

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

Checked nominal proof certificate identified upstream as g_baibr.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gBaibr ph ps ch hyp_baib_1 = NFChoice.DirectNominalPrf.WPPReplay.gBicomd ps ph ch (NFChoice.DirectNominalPrf.WPPReplay.gBaib ph ps ch hyp_baib_1)

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

Checked nominal proof certificate identified upstream as g_pm5_6.

Equations

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

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

Checked nominal proof certificate identified upstream as g_orcanai.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gOrcanai ph ps ch hyp_orcanai_1 = NFChoice.DirectNominalPrf.WPPReplay.gImp ph ps.neg ch (NFChoice.DirectNominalPrf.WPPReplay.gOrd ph ps ch hyp_orcanai_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIntnan (ph ps : SemanticCore.Wff) (hyp_intnan_1 : Nominal.NPrf ph.neg) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWa ps ph).neg

Checked nominal proof certificate identified upstream as g_intnan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIntnanr (ph ps : SemanticCore.Wff) (hyp_intnan_1 : Nominal.NPrf ph.neg) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWa ph ps).neg

Checked nominal proof certificate identified upstream as g_intnanr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_intnand.

Equations

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

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

Checked nominal proof certificate identified upstream as g_intnanrd.

Equations

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

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

Checked nominal proof certificate identified upstream as g_mpbiran.

Equations

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

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

Checked nominal proof certificate identified upstream as g_mpbiran2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_mpbir2an.

Equations

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

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

Checked nominal proof certificate identified upstream as g_bianfi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEcase3 (ph ps ch : SemanticCore.Wff) (hyp_ecase3_1 : Nominal.NPrf (ph.imp ch)) (hyp_ecase3_2 : Nominal.NPrf (ps.imp ch)) (hyp_ecase3_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWo ph ps).neg.imp ch)) : Nominal.NPrf ch

Checked nominal proof certificate identified upstream as g_ecase3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dedlem0a.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dedlema.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dedlemb.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pm4_42.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOplem1 (ph ps ch th ta : SemanticCore.Wff) (hyp_oplem1_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo ps ch))) (hyp_oplem1_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWo th ta))) (hyp_oplem1_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps th)) (hyp_oplem1_4 : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWb th ta))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_oplem1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3orass.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3anass.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3anrot.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3orrot.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3ancoma.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3ancomb.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3anrev.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3simpa.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3simpb.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3simpc.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpl1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpl2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpl3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpr1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp1d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp2d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp3d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp1bi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp2bi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp3bi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3adant1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3adant2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3adant3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3ad2ant1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3ad2ant2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3ad2ant3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp1l.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp1r.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp2l.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp2r.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp3l.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp3r.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp21.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp23.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp31.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp32.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp33.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpl1l.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpl1r.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpl2l.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpl2r.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpl3l.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpl3r.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpr2l.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpr2r.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpr3l.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpr3r.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp1rl.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp1rr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp2ll.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp2lr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp2rl.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp2rr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp3ll.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp3lr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp3rl.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp3rr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpl31.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simpl32.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp12l.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp12r.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp22r.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simp23l.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3adantl1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3adantl2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3adantr1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3ad2antl1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3ad2antl3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3mix1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3mix2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3mix3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3pm32i (ph ps ch : SemanticCore.Wff) (hyp_n_3pm3_2i_1 : Nominal.NPrf ph) (hyp_n_3pm3_2i_2 : Nominal.NPrf ps) (hyp_n_3pm3_2i_3 : Nominal.NPrf ch) : Nominal.NPrf (Compiler.CompactSourceSyntax.synW3a ph ps ch)

Checked nominal proof certificate identified upstream as g_n_3pm3_2i.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pm3_2an3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3jca (ph ps ch th : SemanticCore.Wff) (hyp_n_3jca_1 : Nominal.NPrf (ph.imp ps)) (hyp_n_3jca_2 : Nominal.NPrf (ph.imp ch)) (hyp_n_3jca_3 : Nominal.NPrf (ph.imp th)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synW3a ps ch th))

Checked nominal proof certificate identified upstream as g_n_3jca.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3jcad (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3jcad_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_n_3jcad_2 : Nominal.NPrf (ph.imp (ps.imp th))) (hyp_n_3jcad_3 : Nominal.NPrf (ph.imp (ps.imp ta))) : Nominal.NPrf (ph.imp (ps.imp (Compiler.CompactSourceSyntax.synW3a ch th ta)))

Checked nominal proof certificate identified upstream as g_n_3jcad.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMpbir3an (ph ps ch th : SemanticCore.Wff) (hyp_mpbir3an_1 : Nominal.NPrf ps) (hyp_mpbir3an_2 : Nominal.NPrf ch) (hyp_mpbir3an_3 : Nominal.NPrf th) (hyp_mpbir3an_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synW3a ps ch th))) : Nominal.NPrf ph

Checked nominal proof certificate identified upstream as g_mpbir3an.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl3anbrc (ph ps ch th ta : SemanticCore.Wff) (hyp_syl3anbrc_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl3anbrc_2 : Nominal.NPrf (ph.imp ch)) (hyp_syl3anbrc_3 : Nominal.NPrf (ph.imp th)) (hyp_syl3anbrc_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ta (Compiler.CompactSourceSyntax.synW3a ps ch th))) : Nominal.NPrf (ph.imp ta)

Checked nominal proof certificate identified upstream as g_syl3anbrc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3anim123i (ph ps ch th ta et : SemanticCore.Wff) (hyp_n_3anim123i_1 : Nominal.NPrf (ph.imp ps)) (hyp_n_3anim123i_2 : Nominal.NPrf (ch.imp th)) (hyp_n_3anim123i_3 : Nominal.NPrf (ta.imp et)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph ch ta).imp (Compiler.CompactSourceSyntax.synW3a ps th et))

Checked nominal proof certificate identified upstream as g_n_3anim123i.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3anim1i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3anbi123i (ph ps ch th ta et : SemanticCore.Wff) (hyp_bi3_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) (hyp_bi3_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ch th)) (hyp_bi3_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ta et)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3a ph ch ta) (Compiler.CompactSourceSyntax.synW3a ps th et))

Checked nominal proof certificate identified upstream as g_n_3anbi123i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3anbi1i (ph ps ch th : SemanticCore.Wff) (hyp_n_3anbi1i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3a ph ch th) (Compiler.CompactSourceSyntax.synW3a ps ch th))

Checked nominal proof certificate identified upstream as g_n_3anbi1i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3anbi2i (ph ps ch th : SemanticCore.Wff) (hyp_n_3anbi1i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3a ch ph th) (Compiler.CompactSourceSyntax.synW3a ch ps th))

Checked nominal proof certificate identified upstream as g_n_3anbi2i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3anbi3i (ph ps ch th : SemanticCore.Wff) (hyp_n_3anbi1i_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3a ch th ph) (Compiler.CompactSourceSyntax.synW3a ch th ps))

Checked nominal proof certificate identified upstream as g_n_3anbi3i.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3imp.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3impa.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3impb.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3impia.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3impib.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3exp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3expa (ph ps ch th : SemanticCore.Wff) (hyp_n_3exp_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph 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_n_3expa.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3expb (ph ps ch th : SemanticCore.Wff) (hyp_n_3exp_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a 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_n_3expb.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3expia.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3expib.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3com12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3com13.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3com23.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3coml.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3impd (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3imp1_1 : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synW3a ps ch th).imp ta))

Checked nominal proof certificate identified upstream as g_n_3impd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3expd (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3expd_1 : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synW3a ps ch th).imp ta))) : Nominal.NPrf (ph.imp (ps.imp (ch.imp (th.imp ta))))

Checked nominal proof certificate identified upstream as g_n_3expd.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3exp2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3adant1r.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl12anc (ph ps ch th ta : SemanticCore.Wff) (hyp_sylXanc_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylXanc_2 : Nominal.NPrf (ph.imp ch)) (hyp_sylXanc_3 : Nominal.NPrf (ph.imp th)) (hyp_syl12anc_4 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps (Compiler.CompactSourceSyntax.synWa ch th)).imp ta)) : Nominal.NPrf (ph.imp ta)

Checked nominal proof certificate identified upstream as g_syl12anc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl21anc (ph ps ch th ta : SemanticCore.Wff) (hyp_sylXanc_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylXanc_2 : Nominal.NPrf (ph.imp ch)) (hyp_sylXanc_3 : Nominal.NPrf (ph.imp th)) (hyp_syl21anc_4 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ps ch) th).imp ta)) : Nominal.NPrf (ph.imp ta)

Checked nominal proof certificate identified upstream as g_syl21anc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl3anc (ph ps ch th ta : SemanticCore.Wff) (hyp_sylXanc_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylXanc_2 : Nominal.NPrf (ph.imp ch)) (hyp_sylXanc_3 : Nominal.NPrf (ph.imp th)) (hyp_syl111anc_4 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ps ch th).imp ta)) : Nominal.NPrf (ph.imp ta)

Checked nominal proof certificate identified upstream as g_syl3anc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl22anc (ph ps ch th ta et : SemanticCore.Wff) (hyp_sylXanc_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylXanc_2 : Nominal.NPrf (ph.imp ch)) (hyp_sylXanc_3 : Nominal.NPrf (ph.imp th)) (hyp_sylXanc_4 : Nominal.NPrf (ph.imp ta)) (hyp_syl22anc_5 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ps ch) (Compiler.CompactSourceSyntax.synWa th ta)).imp et)) : Nominal.NPrf (ph.imp et)

Checked nominal proof certificate identified upstream as g_syl22anc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl13anc (ph ps ch th ta et : SemanticCore.Wff) (hyp_sylXanc_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylXanc_2 : Nominal.NPrf (ph.imp ch)) (hyp_sylXanc_3 : Nominal.NPrf (ph.imp th)) (hyp_sylXanc_4 : Nominal.NPrf (ph.imp ta)) (hyp_syl13anc_5 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps (Compiler.CompactSourceSyntax.synW3a ch th ta)).imp et)) : Nominal.NPrf (ph.imp et)

Checked nominal proof certificate identified upstream as g_syl13anc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl31anc (ph ps ch th ta et : SemanticCore.Wff) (hyp_sylXanc_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylXanc_2 : Nominal.NPrf (ph.imp ch)) (hyp_sylXanc_3 : Nominal.NPrf (ph.imp th)) (hyp_sylXanc_4 : Nominal.NPrf (ph.imp ta)) (hyp_syl31anc_5 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a ps ch th) ta).imp et)) : Nominal.NPrf (ph.imp et)

Checked nominal proof certificate identified upstream as g_syl31anc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl211anc (ph ps ch th ta et : SemanticCore.Wff) (hyp_sylXanc_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylXanc_2 : Nominal.NPrf (ph.imp ch)) (hyp_sylXanc_3 : Nominal.NPrf (ph.imp th)) (hyp_sylXanc_4 : Nominal.NPrf (ph.imp ta)) (hyp_syl211anc_5 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWa ps ch) th ta).imp et)) : Nominal.NPrf (ph.imp et)

Checked nominal proof certificate identified upstream as g_syl211anc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl221anc (ph ps ch th ta et ze : SemanticCore.Wff) (hyp_sylXanc_1 : Nominal.NPrf (ph.imp ps)) (hyp_sylXanc_2 : Nominal.NPrf (ph.imp ch)) (hyp_sylXanc_3 : Nominal.NPrf (ph.imp th)) (hyp_sylXanc_4 : Nominal.NPrf (ph.imp ta)) (hyp_sylXanc_5 : Nominal.NPrf (ph.imp et)) (hyp_syl221anc_6 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWa ps ch) (Compiler.CompactSourceSyntax.synWa th ta) et).imp ze)) : Nominal.NPrf (ph.imp ze)

Checked nominal proof certificate identified upstream as g_syl221anc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl3an1 (ph ps ch th ta : SemanticCore.Wff) (hyp_syl3an1_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl3an1_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ps ch th).imp ta)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph ch th).imp ta)

Checked nominal proof certificate identified upstream as g_syl3an1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl3an3 (ph ps ch th ta : SemanticCore.Wff) (hyp_syl3an3_1 : Nominal.NPrf (ph.imp th)) (hyp_syl3an3_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ps ch th).imp ta)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ps ch ph).imp ta)

Checked nominal proof certificate identified upstream as g_syl3an3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl3an3b (ph ps ch th ta : SemanticCore.Wff) (hyp_syl3an3b_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph th)) (hyp_syl3an3b_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ps ch th).imp ta)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ps ch ph).imp ta)

Checked nominal proof certificate identified upstream as g_syl3an3b.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl3an (ph ps ch th ta et ze : SemanticCore.Wff) (hyp_syl3an_1 : Nominal.NPrf (ph.imp ps)) (hyp_syl3an_2 : Nominal.NPrf (ch.imp th)) (hyp_syl3an_3 : Nominal.NPrf (ta.imp et)) (hyp_syl3an_4 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ps th et).imp ze)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph ch ta).imp ze)

Checked nominal proof certificate identified upstream as g_syl3an.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3anidm12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3anidm13.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3anidm23.

Equations

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

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

Checked nominal proof certificate identified upstream as g_n_3jao.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3jaoi (ph ps ch th : SemanticCore.Wff) (hyp_n_3jaoi_1 : Nominal.NPrf (ph.imp ps)) (hyp_n_3jaoi_2 : Nominal.NPrf (ch.imp ps)) (hyp_n_3jaoi_3 : Nominal.NPrf (th.imp ps)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3o ph ch th).imp ps)

Checked nominal proof certificate identified upstream as g_n_3jaoi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3jaod (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3jaod_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_n_3jaod_2 : Nominal.NPrf (ph.imp (th.imp ch))) (hyp_n_3jaod_3 : Nominal.NPrf (ph.imp (ta.imp ch))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synW3o ps th ta).imp ch))

Checked nominal proof certificate identified upstream as g_n_3jaod.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl3an9b (ph ps ch th ta et ze : SemanticCore.Wff) (hyp_syl3an9b_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_syl3an9b_2 : Nominal.NPrf (th.imp (Compiler.CompactSourceSyntax.synWb ch ta))) (hyp_syl3an9b_3 : Nominal.NPrf (et.imp (Compiler.CompactSourceSyntax.synWb ta ze))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph th et).imp (Compiler.CompactSourceSyntax.synWb ps ze))

Checked nominal proof certificate identified upstream as g_syl3an9b.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3orbi123d (ph ps ch th ta et ze : SemanticCore.Wff) (hyp_bi3d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_bi3d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))) (hyp_bi3d_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb et ze))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3o ps th et) (Compiler.CompactSourceSyntax.synW3o ch ta ze)))

Checked nominal proof certificate identified upstream as g_n_3orbi123d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3anbi123d (ph ps ch th ta et ze : SemanticCore.Wff) (hyp_bi3d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_bi3d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))) (hyp_bi3d_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb et ze))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3a ps th et) (Compiler.CompactSourceSyntax.synW3a ch ta ze)))

Checked nominal proof certificate identified upstream as g_n_3anbi123d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3anbi12d (ph ps ch th ta et : SemanticCore.Wff) (hyp_n_3anbi12d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_n_3anbi12d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3a ps th et) (Compiler.CompactSourceSyntax.synW3a ch ta et)))

Checked nominal proof certificate identified upstream as g_n_3anbi12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3anbi13d (ph ps ch th ta et : SemanticCore.Wff) (hyp_n_3anbi12d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_n_3anbi12d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3a ps et th) (Compiler.CompactSourceSyntax.synW3a ch et ta)))

Checked nominal proof certificate identified upstream as g_n_3anbi13d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3anbi23d (ph ps ch th ta et : SemanticCore.Wff) (hyp_n_3anbi12d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_n_3anbi12d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3a et ps th) (Compiler.CompactSourceSyntax.synW3a et ch ta)))

Checked nominal proof certificate identified upstream as g_n_3anbi23d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3anbi1d (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3anbi1d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3a ps th ta) (Compiler.CompactSourceSyntax.synW3a ch th ta)))

Checked nominal proof certificate identified upstream as g_n_3anbi1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3anbi2d (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3anbi1d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3a th ps ta) (Compiler.CompactSourceSyntax.synW3a th ch ta)))

Checked nominal proof certificate identified upstream as g_n_3anbi2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3anbi3d (ph ps ch th ta : SemanticCore.Wff) (hyp_n_3anbi1d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3a th ta ps) (Compiler.CompactSourceSyntax.synW3a th ta ch)))

Checked nominal proof certificate identified upstream as g_n_3anbi3d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3orim123d (ph ps ch th ta et ze : SemanticCore.Wff) (hyp_n_3anim123d_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_n_3anim123d_2 : Nominal.NPrf (ph.imp (th.imp ta))) (hyp_n_3anim123d_3 : Nominal.NPrf (ph.imp (et.imp ze))) : Nominal.NPrf (ph.imp ((Compiler.CompactSourceSyntax.synW3o ps th et).imp (Compiler.CompactSourceSyntax.synW3o ch ta ze)))

Checked nominal proof certificate identified upstream as g_n_3orim123d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAn6 (ph ps ch th ta et : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a ph ps ch) (Compiler.CompactSourceSyntax.synW3a th ta et)) (Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWa ph th) (Compiler.CompactSourceSyntax.synWa ps ta) (Compiler.CompactSourceSyntax.synWa ch et)))

Checked nominal proof certificate identified upstream as g_an6.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3an6 (ph ps ch th ta et : SemanticCore.Wff) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWa ph ps) (Compiler.CompactSourceSyntax.synWa ch th) (Compiler.CompactSourceSyntax.synWa ta et)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a ph ch ta) (Compiler.CompactSourceSyntax.synW3a ps th et)))

Checked nominal proof certificate identified upstream as g_n_3an6.

Equations

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

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

Checked nominal proof certificate identified upstream as g_mp3an1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_mp3an2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_mp3an3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMp3an12 (ph ps ch th : SemanticCore.Wff) (hyp_mp3an12_1 : Nominal.NPrf ph) (hyp_mp3an12_2 : Nominal.NPrf ps) (hyp_mp3an12_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph ps ch).imp th)) : Nominal.NPrf (ch.imp th)

Checked nominal proof certificate identified upstream as g_mp3an12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMp3an13 (ph ps ch th : SemanticCore.Wff) (hyp_mp3an13_1 : Nominal.NPrf ph) (hyp_mp3an13_2 : Nominal.NPrf ch) (hyp_mp3an13_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph ps ch).imp th)) : Nominal.NPrf (ps.imp th)

Checked nominal proof certificate identified upstream as g_mp3an13.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMp3an23 (ph ps ch th : SemanticCore.Wff) (hyp_mp3an23_1 : Nominal.NPrf ps) (hyp_mp3an23_2 : Nominal.NPrf ch) (hyp_mp3an23_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph ps ch).imp th)) : Nominal.NPrf (ph.imp th)

Checked nominal proof certificate identified upstream as g_mp3an23.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMp3an (ph ps ch th : SemanticCore.Wff) (hyp_mp3an_1 : Nominal.NPrf ph) (hyp_mp3an_2 : Nominal.NPrf ps) (hyp_mp3an_3 : Nominal.NPrf ch) (hyp_mp3an_4 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph ps ch).imp th)) : Nominal.NPrf th

Checked nominal proof certificate identified upstream as g_mp3an.

Equations

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

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

Checked nominal proof certificate identified upstream as g_mpd3an3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEcase23d (ph ps ch th : SemanticCore.Wff) (hyp_ecase23d_1 : Nominal.NPrf (ph.imp ch.neg)) (hyp_ecase23d_2 : Nominal.NPrf (ph.imp th.neg)) (hyp_ecase23d_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synW3o ps ch th))) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_ecase23d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nancom.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nanbi1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nanbi2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nanbi12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNanbi2i (ph ps ch : SemanticCore.Wff) (hyp_nanbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWnan ch ph) (Compiler.CompactSourceSyntax.synWnan ch ps))

Checked nominal proof certificate identified upstream as g_nanbi2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNanbi2i ph ps ch hyp_nanbii_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_nanbii_1 (NFChoice.DirectNominalPrf.WPPReplay.gNanbi2 ph ps ch)

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

Checked nominal proof certificate identified upstream as g_nanbi1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNanbi12d (ph ps ch th ta : SemanticCore.Wff) (hyp_nanbid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_nanbi12d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb th ta))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWnan ps th) (Compiler.CompactSourceSyntax.synWnan ch ta)))

Checked nominal proof certificate identified upstream as g_nanbi12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTru : Nominal.NPrf Compiler.CompactSourceSyntax.synWtru

Checked nominal proof certificate identified upstream as g_tru.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTrud (ph : SemanticCore.Wff) (hyp_trud_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWtru.imp ph)) : Nominal.NPrf ph

Checked nominal proof certificate identified upstream as g_trud.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gTrud ph hyp_trud_1 = NFChoice.DirectNominalPrf.Nominal.mp NFChoice.DirectNominalPrf.WPPReplay.gTru hyp_trud_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEe22 (ph ps ch th ta : SemanticCore.Wff) (hyp_ee22_1 : Nominal.NPrf (ph.imp (ps.imp ch))) (hyp_ee22_2 : Nominal.NPrf (ph.imp (ps.imp th))) (hyp_ee22_3 : Nominal.NPrf (ch.imp (th.imp ta))) : Nominal.NPrf (ph.imp (ps.imp ta))

Checked nominal proof certificate identified upstream as g_ee22.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gEe22 ph ps ch th ta hyp_ee22_1 hyp_ee22_2 hyp_ee22_3 = NFChoice.DirectNominalPrf.WPPReplay.gSyl6c ph ps ch th ta hyp_ee22_1 hyp_ee22_2 hyp_ee22_3

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

Checked nominal proof certificate identified upstream as g_ancomsimp.

Equations

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

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

Checked nominal proof certificate identified upstream as g_exp3acom23.

Equations

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

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

Checked nominal proof certificate identified upstream as g_simplbi2com.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEe10 (ph ps ch th : SemanticCore.Wff) (hyp_ee10_1 : Nominal.NPrf (ph.imp ps)) (hyp_ee10_2 : Nominal.NPrf ch) (hyp_ee10_3 : Nominal.NPrf (ps.imp (ch.imp th))) : Nominal.NPrf (ph.imp th)

Checked nominal proof certificate identified upstream as g_ee10.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEe02 (ph ps ch th ta : SemanticCore.Wff) (hyp_ee02_1 : Nominal.NPrf ph) (hyp_ee02_2 : Nominal.NPrf (ps.imp (ch.imp th))) (hyp_ee02_3 : Nominal.NPrf (ph.imp (th.imp ta))) : Nominal.NPrf (ps.imp (ch.imp ta))

Checked nominal proof certificate identified upstream as g_ee02.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMerlem1 (ph ps ch ta : SemanticCore.Wff) : Nominal.NPrf (((ch.imp (ph.neg.imp ps)).imp ta).imp (ph.imp ta))

Checked nominal proof certificate identified upstream as g_merlem1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMerlem2 (ph ch th : SemanticCore.Wff) : Nominal.NPrf (((ph.imp ph).imp ch).imp (th.imp ch))

Checked nominal proof certificate identified upstream as g_merlem2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMerlem3 (ph ps ch : SemanticCore.Wff) : Nominal.NPrf (((ps.imp ch).imp ph).imp (ch.imp ph))

Checked nominal proof certificate identified upstream as g_merlem3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMerlem4 (ph th ta : SemanticCore.Wff) : Nominal.NPrf (ta.imp ((ta.imp ph).imp (th.imp ph)))

Checked nominal proof certificate identified upstream as g_merlem4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMerlem5 (ph ps : SemanticCore.Wff) : Nominal.NPrf ((ph.imp ps).imp (ph.neg.neg.imp ps))

Checked nominal proof certificate identified upstream as g_merlem5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMerlem6 (ph ps ch th : SemanticCore.Wff) : Nominal.NPrf (ch.imp (((ps.imp ch).imp ph).imp (th.imp ph)))

Checked nominal proof certificate identified upstream as g_merlem6.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMerlem7 (ph ps ch th ta : SemanticCore.Wff) : Nominal.NPrf (ph.imp (((ps.imp ch).imp th).imp (((ch.imp ta).imp (th.neg.imp ps.neg)).imp th)))

Checked nominal proof certificate identified upstream as g_merlem7.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMerlem8 (ps ch th ta : SemanticCore.Wff) : Nominal.NPrf (((ps.imp ch).imp th).imp (((ch.imp ta).imp (th.neg.imp ps.neg)).imp th))

Checked nominal proof certificate identified upstream as g_merlem8.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMerlem9 (ph ps ch th ta et : SemanticCore.Wff) : Nominal.NPrf (((ph.imp ps).imp (ch.imp (th.imp (ps.imp ta)))).imp (et.imp (ch.imp (th.imp (ps.imp ta)))))

Checked nominal proof certificate identified upstream as g_merlem9.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gMerlem10 (ph ps th : SemanticCore.Wff) : Nominal.NPrf ((ph.imp (ph.imp ps)).imp (th.imp (ph.imp ps)))

Checked nominal proof certificate identified upstream as g_merlem10.

Equations

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