NF weak partition development: NominalWPPReplayChunk008.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDedth2h (ph ps ch th ta : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_dedth2h_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A C)).imp (Compiler.CompactSourceSyntax.synWb ch th))) (hyp_dedth2h_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ps B D)).imp (Compiler.CompactSourceSyntax.synWb th ta))) (hyp_dedth2h_3 : Nominal.NPrf ta) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp ch)

Checked nominal proof certificate identified upstream as g_dedth2h.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDedth3h (ph ps ch th ta et ze : SemanticCore.Wff) (A B C D R S : SemanticCore.Class) (hyp_dedth3h_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A D)).imp (Compiler.CompactSourceSyntax.synWb th ta))) (hyp_dedth3h_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ps B R)).imp (Compiler.CompactSourceSyntax.synWb ta et))) (hyp_dedth3h_3 : Nominal.NPrf ((SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCif ch C S)).imp (Compiler.CompactSourceSyntax.synWb et ze))) (hyp_dedth3h_4 : Nominal.NPrf ze) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a ph ps ch).imp th)

Checked nominal proof certificate identified upstream as g_dedth3h.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDedth4h (ph ps ch th ta et ze si rh : SemanticCore.Wff) (A B C D R S F G : SemanticCore.Class) (hyp_dedth4h_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A R)).imp (Compiler.CompactSourceSyntax.synWb ta et))) (hyp_dedth4h_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ps B S)).imp (Compiler.CompactSourceSyntax.synWb et ze))) (hyp_dedth4h_3 : Nominal.NPrf ((SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCif ch C F)).imp (Compiler.CompactSourceSyntax.synWb ze si))) (hyp_dedth4h_4 : Nominal.NPrf ((SemanticCore.Wff.classEq D (Compiler.CompactSourceSyntax.synCif th D G)).imp (Compiler.CompactSourceSyntax.synWb si rh))) (hyp_dedth4h_5 : Nominal.NPrf rh) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa ph ps) (Compiler.CompactSourceSyntax.synWa ch th)).imp ta)

Checked nominal proof certificate identified upstream as g_dedth4h.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDedth2v (ph ps ch th : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_dedth2v_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A C)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_dedth2v_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ph B D)).imp (Compiler.CompactSourceSyntax.synWb ch th))) (hyp_dedth2v_3 : Nominal.NPrf th) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_dedth2v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDedth3v (ph ps ch th ta : SemanticCore.Wff) (A B C D R S : SemanticCore.Class) (hyp_dedth3v_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A D)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_dedth3v_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ph B R)).imp (Compiler.CompactSourceSyntax.synWb ch th))) (hyp_dedth3v_3 : Nominal.NPrf ((SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCif ph C S)).imp (Compiler.CompactSourceSyntax.synWb th ta))) (hyp_dedth3v_4 : Nominal.NPrf ta) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_dedth3v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDedth4v (ph ps ch th ta et : SemanticCore.Wff) (A B C D R S T U : SemanticCore.Class) (hyp_dedth4v_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A R)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_dedth4v_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ph B S)).imp (Compiler.CompactSourceSyntax.synWb ch th))) (hyp_dedth4v_3 : Nominal.NPrf ((SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCif ph C T)).imp (Compiler.CompactSourceSyntax.synWb th ta))) (hyp_dedth4v_4 : Nominal.NPrf ((SemanticCore.Wff.classEq D (Compiler.CompactSourceSyntax.synCif ph D U)).imp (Compiler.CompactSourceSyntax.synWb ta et))) (hyp_dedth4v_5 : Nominal.NPrf et) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_dedth4v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimhyp2v (ph ch th ta et : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_elimhyp2v_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A C)).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_elimhyp2v_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ph B D)).imp (Compiler.CompactSourceSyntax.synWb ch th))) (hyp_elimhyp2v_3 : Nominal.NPrf ((SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCif ph A C)).imp (Compiler.CompactSourceSyntax.synWb ta et))) (hyp_elimhyp2v_4 : Nominal.NPrf ((SemanticCore.Wff.classEq D (Compiler.CompactSourceSyntax.synCif ph B D)).imp (Compiler.CompactSourceSyntax.synWb et th))) (hyp_elimhyp2v_5 : Nominal.NPrf ta) : Nominal.NPrf th

Checked nominal proof certificate identified upstream as g_elimhyp2v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimhyp3v (ph ch th ta et ze si : SemanticCore.Wff) (A B C D R S : SemanticCore.Class) (hyp_elimhyp3v_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A D)).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_elimhyp3v_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ph B R)).imp (Compiler.CompactSourceSyntax.synWb ch th))) (hyp_elimhyp3v_3 : Nominal.NPrf ((SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCif ph C S)).imp (Compiler.CompactSourceSyntax.synWb th ta))) (hyp_elimhyp3v_4 : Nominal.NPrf ((SemanticCore.Wff.classEq D (Compiler.CompactSourceSyntax.synCif ph A D)).imp (Compiler.CompactSourceSyntax.synWb et ze))) (hyp_elimhyp3v_5 : Nominal.NPrf ((SemanticCore.Wff.classEq R (Compiler.CompactSourceSyntax.synCif ph B R)).imp (Compiler.CompactSourceSyntax.synWb ze si))) (hyp_elimhyp3v_6 : Nominal.NPrf ((SemanticCore.Wff.classEq S (Compiler.CompactSourceSyntax.synCif ph C S)).imp (Compiler.CompactSourceSyntax.synWb si ta))) (hyp_elimhyp3v_7 : Nominal.NPrf et) : Nominal.NPrf ta

Checked nominal proof certificate identified upstream as g_elimhyp3v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimhyp4v (ph ps ch th ta et ze si rh : SemanticCore.Wff) (A B C D R S F G : SemanticCore.Class) (hyp_elimhyp4v_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A D)).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_elimhyp4v_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ph B R)).imp (Compiler.CompactSourceSyntax.synWb ch th))) (hyp_elimhyp4v_3 : Nominal.NPrf ((SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCif ph C S)).imp (Compiler.CompactSourceSyntax.synWb th ta))) (hyp_elimhyp4v_4 : Nominal.NPrf ((SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCif ph F G)).imp (Compiler.CompactSourceSyntax.synWb ta ps))) (hyp_elimhyp4v_5 : Nominal.NPrf ((SemanticCore.Wff.classEq D (Compiler.CompactSourceSyntax.synCif ph A D)).imp (Compiler.CompactSourceSyntax.synWb et ze))) (hyp_elimhyp4v_6 : Nominal.NPrf ((SemanticCore.Wff.classEq R (Compiler.CompactSourceSyntax.synCif ph B R)).imp (Compiler.CompactSourceSyntax.synWb ze si))) (hyp_elimhyp4v_7 : Nominal.NPrf ((SemanticCore.Wff.classEq S (Compiler.CompactSourceSyntax.synCif ph C S)).imp (Compiler.CompactSourceSyntax.synWb si rh))) (hyp_elimhyp4v_8 : Nominal.NPrf ((SemanticCore.Wff.classEq G (Compiler.CompactSourceSyntax.synCif ph F G)).imp (Compiler.CompactSourceSyntax.synWb rh ps))) (hyp_elimhyp4v_9 : Nominal.NPrf et) : Nominal.NPrf ps

Checked nominal proof certificate identified upstream as g_elimhyp4v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKeephyp (ph ps ch th : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_keephyp_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A B)).imp (Compiler.CompactSourceSyntax.synWb ps th))) (hyp_keephyp_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ph A B)).imp (Compiler.CompactSourceSyntax.synWb ch th))) (hyp_keephyp_3 : Nominal.NPrf ps) (hyp_keephyp_4 : Nominal.NPrf ch) : Nominal.NPrf th

Checked nominal proof certificate identified upstream as g_keephyp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKeephyp2v (ph ps ch th ta et : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_keephyp2v_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A C)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_keephyp2v_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ph B D)).imp (Compiler.CompactSourceSyntax.synWb ch th))) (hyp_keephyp2v_3 : Nominal.NPrf ((SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCif ph A C)).imp (Compiler.CompactSourceSyntax.synWb ta et))) (hyp_keephyp2v_4 : Nominal.NPrf ((SemanticCore.Wff.classEq D (Compiler.CompactSourceSyntax.synCif ph B D)).imp (Compiler.CompactSourceSyntax.synWb et th))) (hyp_keephyp2v_5 : Nominal.NPrf ps) (hyp_keephyp2v_6 : Nominal.NPrf ta) : Nominal.NPrf th

Checked nominal proof certificate identified upstream as g_keephyp2v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKeepel (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_keepel_1 : Nominal.NPrf (SemanticCore.Wff.classMem A C)) (hyp_keepel_2 : Nominal.NPrf (SemanticCore.Wff.classMem B C)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCif ph A B) C)

Checked nominal proof certificate identified upstream as g_keepel.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfex (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_dedex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_dedex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCif ph A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ifex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pweq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPweqi (A B : SemanticCore.Class) (hyp_pweqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpw A) (Compiler.CompactSourceSyntax.synCpw B))

Checked nominal proof certificate identified upstream as g_pweqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gPweqi A B hyp_pweqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_pweqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gPweq A B)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPweqd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_pweqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpw A) (Compiler.CompactSourceSyntax.synCpw B)))

Checked nominal proof certificate identified upstream as g_pweqd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpw (A B : SemanticCore.Class) (hyp_elpw_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCpw B)) (Compiler.CompactSourceSyntax.synWss A B))

Checked nominal proof certificate identified upstream as g_elpw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpwg (A B V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCpw B)) (Compiler.CompactSourceSyntax.synWss A B)))

Checked nominal proof certificate identified upstream as g_elpwg.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sneq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSneqi (A B : SemanticCore.Class) (hyp_sneqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCsn B))

Checked nominal proof certificate identified upstream as g_sneqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSneqi A B hyp_sneqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_sneqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gSneq A B)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSneqd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_sneqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCsn B)))

Checked nominal proof certificate identified upstream as g_sneqd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfsn2 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCpr A A))

Checked nominal proof certificate identified upstream as g_dfsn2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elsn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfpr2 (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpr A B) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) B))))

Checked nominal proof certificate identified upstream as g_dfpr2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elprg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpr (A B C : SemanticCore.Class) (hyp_elpr_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCpr B C)) (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.classEq A C)))

Checked nominal proof certificate identified upstream as g_elpr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpr2 (A B C : SemanticCore.Class) (hyp_elpr2_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_elpr2_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCpr B C)) (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.classEq A C)))

Checked nominal proof certificate identified upstream as g_elpr2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elsncg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElsnc (A B : SemanticCore.Class) (hyp_elsnc_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCsn B)) (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_elsnc.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elsni.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnidg (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCsn A)))

Checked nominal proof certificate identified upstream as g_snidg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnidb (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCsn A)))

Checked nominal proof certificate identified upstream as g_snidb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnid (A : SemanticCore.Class) (hyp_snid_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCsn A))

Checked nominal proof certificate identified upstream as g_snid.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elsnc2g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElsnc2 (A B : SemanticCore.Class) (hyp_elsnc2_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCsn B)) (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_elsnc2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexsns (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCsn A) ph) (Compiler.CompactSourceSyntax.synWsbc A x ph)))

Checked nominal proof certificate identified upstream as g_rexsns.

Equations

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

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

Checked nominal proof certificate identified upstream as g_rexsng.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexsn (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_ralsn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_ralsn_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCsn A) ph) ps)

Checked nominal proof certificate identified upstream as g_rexsn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDisjsn (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A (Compiler.CompactSourceSyntax.synCsn B)) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classMem B A).neg)

Checked nominal proof certificate identified upstream as g_disjsn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnprc (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).neg (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsn A) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_snprc.

Equations

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

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

Checked nominal proof certificate identified upstream as g_rabsn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_prcom.

Equations

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

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

Checked nominal proof certificate identified upstream as g_preq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_preq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_preq12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPreq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_preq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpr C A) (Compiler.CompactSourceSyntax.synCpr C B)))

Checked nominal proof certificate identified upstream as g_preq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPreq12d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_preq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_preq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpr A C) (Compiler.CompactSourceSyntax.synCpr B D)))

Checked nominal proof certificate identified upstream as g_preq12d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_prid1g.

Equations

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

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

Checked nominal proof certificate identified upstream as g_prid1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnnzg (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCsn A) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_snnzg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnnz (A : SemanticCore.Class) (hyp_snnz_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCsn A) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_snnz.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnss (A B : SemanticCore.Class) (hyp_snss_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A B) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCsn A) B))

Checked nominal proof certificate identified upstream as g_snss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEldifsn (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdif B (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A B) (Compiler.CompactSourceSyntax.synWne A C)))

Checked nominal proof certificate identified upstream as g_eldifsn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEldifsni (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdif B (Compiler.CompactSourceSyntax.synCsn C))).imp (Compiler.CompactSourceSyntax.synWne A C))

Checked nominal proof certificate identified upstream as g_eldifsni.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNeldifsn (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdif B (Compiler.CompactSourceSyntax.synCsn A))).neg

Checked nominal proof certificate identified upstream as g_neldifsn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnssg (A B V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A B) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCsn A) B)))

Checked nominal proof certificate identified upstream as g_snssg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifsn (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A B).neg.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif B (Compiler.CompactSourceSyntax.synCsn A)) B))

Checked nominal proof certificate identified upstream as g_difsn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_snssi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnssd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_snssd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCsn A) B))

Checked nominal proof certificate identified upstream as g_snssd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifsnid (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCdif A (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synCsn B)) A))

Checked nominal proof certificate identified upstream as g_difsnid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSssn (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn B))))

Checked nominal proof certificate identified upstream as g_sssn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sneqr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSneqrg (A B V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCsn B)).imp (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_sneqrg.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sneqbg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSneqb (A B : SemanticCore.Class) (hyp_sneqb_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCsn B)) (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_sneqb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPwv : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpw Compiler.CompactSourceSyntax.synCvv) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_pwv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnsneqsn (A B C : SemanticCore.Class) (hyp_unsneqsn_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synCsn C)).imp (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn B))))

Checked nominal proof certificate identified upstream as g_unsneqsn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dfpss4.

Equations

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

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

Checked nominal proof certificate identified upstream as g_adj11.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfuni2 (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni A) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWrex y A (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_dfuni2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEluni (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCuni B)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A (SemanticCore.Class.cv x)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B))))

Checked nominal proof certificate identified upstream as g_eluni.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eluni2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elunii.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfuni (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_nfuni_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCuni A))

Checked nominal proof certificate identified upstream as g_nfuni.

Equations

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

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

Checked nominal proof certificate identified upstream as g_unieq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnieqi (A B : SemanticCore.Class) (hyp_unieqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni A) (Compiler.CompactSourceSyntax.synCuni B))

Checked nominal proof certificate identified upstream as g_unieqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gUnieqi A B hyp_unieqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_unieqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gUnieq A B)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnieqd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_unieqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni A) (Compiler.CompactSourceSyntax.synCuni B)))

Checked nominal proof certificate identified upstream as g_unieqd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEluniab (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cab x ph))) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A (SemanticCore.Class.cv x)) ph)))

Checked nominal proof certificate identified upstream as g_eluniab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnipr (A B : SemanticCore.Class) (hyp_unipr_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_unipr_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCpr A B)) (Compiler.CompactSourceSyntax.synCun A B))

Checked nominal proof certificate identified upstream as g_unipr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnisn (A : SemanticCore.Class) (hyp_unisn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCsn A)) A)

Checked nominal proof certificate identified upstream as g_unisn.

Equations

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