NF weak partition development: NominalWPPReplayChunk007.

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

Checked nominal proof certificate identified upstream as g_rspcimedv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_rspcdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspcedv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (hyp_rspcdv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A B))) (hyp_rspcdv_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (ch.imp (Compiler.CompactSourceSyntax.synWrex x B ps)))

Checked nominal proof certificate identified upstream as g_rspcedv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspc2 (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B C D : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_x_y : x ≠ y) (hyp_rspc2_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ch)) (hyp_rspc2_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ps)) (hyp_rspc2_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_rspc2_4 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ch ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)).imp ((Compiler.CompactSourceSyntax.synWral x C (Compiler.CompactSourceSyntax.synWral y D ph)).imp ps))

Checked nominal proof certificate identified upstream as g_rspc2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspc2v (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B C D : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_ch_x : x ∉ ch.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_rspc2v_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_rspc2v_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ch ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)).imp ((Compiler.CompactSourceSyntax.synWral x C (Compiler.CompactSourceSyntax.synWral y D ph)).imp ps))

Checked nominal proof certificate identified upstream as g_rspc2v.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspc2va (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B C D : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_ch_x : x ∉ ch.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_rspc2v_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_rspc2v_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ch ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)) (Compiler.CompactSourceSyntax.synWral x C (Compiler.CompactSourceSyntax.synWral y D ph))).imp ps)

Checked nominal proof certificate identified upstream as g_rspc2va.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspc2ev (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B C D : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_ch_x : x ∉ ch.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_rspc2v_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_rspc2v_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ch ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D) ps).imp (Compiler.CompactSourceSyntax.synWrex x C (Compiler.CompactSourceSyntax.synWrex y D ph)))

Checked nominal proof certificate identified upstream as g_rspc2ev.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspc3v (ph ps ch th : SemanticCore.Wff) (x y z : SemanticCore.Var) (A B C R S T : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_C_z : z ∉ C.fv) (dv_R_x : x ∉ R.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_T_x : x ∉ T.fv) (dv_T_y : y ∉ T.fv) (dv_T_z : z ∉ T.fv) (dv_ch_x : x ∉ ch.fv) (dv_ps_z : z ∉ ps.fv) (dv_th_y : y ∉ th.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_rspc3v_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_rspc3v_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ch th))) (hyp_rspc3v_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv z) C).imp (Compiler.CompactSourceSyntax.synWb th ps))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A R) (SemanticCore.Wff.classMem B S) (SemanticCore.Wff.classMem C T)).imp ((Compiler.CompactSourceSyntax.synWral x R (Compiler.CompactSourceSyntax.synWral y S (Compiler.CompactSourceSyntax.synWral z T ph))).imp ps))

Checked nominal proof certificate identified upstream as g_rspc3v.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqvinc.

Equations

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

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

Checked nominal proof certificate identified upstream as g_alexeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCeqex (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) ph))))

Checked nominal proof certificate identified upstream as g_ceqex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCeqsexg (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_ceqsexg_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_ceqsexg_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) ph)) ps))

Checked nominal proof certificate identified upstream as g_ceqsexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCeqsexgv (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_ceqsexgv_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.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) ph)) ps))

Checked nominal proof certificate identified upstream as g_ceqsexgv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ceqsrexv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_clel2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_clel3g.

Equations

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

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

Checked nominal proof certificate identified upstream as g_clel3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElabgf (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_elabgf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_elabgf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_elabgf_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.classMem A B).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (SemanticCore.Class.cab x ph)) ps))

Checked nominal proof certificate identified upstream as g_elabgf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElabf (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_elabf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_elabf_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_elabf_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (SemanticCore.Class.cab x ph)) ps)

Checked nominal proof certificate identified upstream as g_elabf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElab (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_elab_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_elab_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (SemanticCore.Class.cab x ph)) ps)

Checked nominal proof certificate identified upstream as g_elab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElabg (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_elabg_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 (SemanticCore.Wff.classMem A (SemanticCore.Class.cab x ph)) ps))

Checked nominal proof certificate identified upstream as g_elabg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElab2g (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_elab2g_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_elab2g_2 : Nominal.NPrf (SemanticCore.Wff.classEq B (SemanticCore.Class.cab x ph))) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A B) ps))

Checked nominal proof certificate identified upstream as g_elab2g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElab2 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_elab2_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_elab2_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_elab2_3 : Nominal.NPrf (SemanticCore.Wff.classEq B (SemanticCore.Class.cab x ph))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A B) ps)

Checked nominal proof certificate identified upstream as g_elab2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElab3gf (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_elab3gf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_elab3gf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_elab3gf_3 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((ps.imp (SemanticCore.Wff.classMem A B)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (SemanticCore.Class.cab x ph)) ps))

Checked nominal proof certificate identified upstream as g_elab3gf.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elab3g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElab3 (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_elab3_1 : Nominal.NPrf (ps.imp (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv))) (hyp_elab3_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (SemanticCore.Class.cab x ph)) ps)

Checked nominal proof certificate identified upstream as g_elab3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElrabf (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_elrabf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_elrabf_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) (hyp_elrabf_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_elrabf_4 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCrab x B ph)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A B) ps))

Checked nominal proof certificate identified upstream as g_elrabf.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elrab.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elrab2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalab (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_ralab_1 : Nominal.NPrf ((SemanticCore.Wff.objEq y x).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x (SemanticCore.Class.cab y ph) ch) (SemanticCore.Wff.all x (ps.imp ch)))

Checked nominal proof certificate identified upstream as g_ralab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexab (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_ralab_1 : Nominal.NPrf ((SemanticCore.Wff.objEq y x).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x (SemanticCore.Class.cab y ph) ch) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa ps ch)))

Checked nominal proof certificate identified upstream as g_rexab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRexrab (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_ralab_1 : Nominal.NPrf ((SemanticCore.Wff.objEq y x).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCrab y A ph) ch) (Compiler.CompactSourceSyntax.synWrex x A (Compiler.CompactSourceSyntax.synWa ps ch)))

Checked nominal proof certificate identified upstream as g_rexrab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRalab2 (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ch_x : x ∉ ch.fv) (dv_ph_x : x ∉ ph.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_ralab2_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x (SemanticCore.Class.cab y ph) ps) (SemanticCore.Wff.all y (ph.imp ch)))

Checked nominal proof certificate identified upstream as g_ralab2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAbidnf (x z : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_z : z ∉ A.fv) (dv_x_z : x ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWnfc x A).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cab z (SemanticCore.Wff.all x (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) A))) A))

Checked nominal proof certificate identified upstream as g_abidnf.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eueq.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eueq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_moeq.

Equations

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

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

Checked nominal proof certificate identified upstream as g_rmo4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReu4 (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_rmo4_1 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWreu x A ph) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWrex x A ph) (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y A ((Compiler.CompactSourceSyntax.synWa ph ps).imp (SemanticCore.Wff.objEq x y))))))

Checked nominal proof certificate identified upstream as g_reu4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfsbcq (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsbc A x ph) (Compiler.CompactSourceSyntax.synWsbc B x ph)))

Checked nominal proof certificate identified upstream as g_dfsbcq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfsbcq2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) A).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsb y x ph) (Compiler.CompactSourceSyntax.synWsbc A x ph)))

Checked nominal proof certificate identified upstream as g_dfsbcq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sbsbc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbcex (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWsbc A x ph).imp (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_sbcex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSpsbc (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp ((SemanticCore.Wff.all x ph).imp (Compiler.CompactSourceSyntax.synWsbc A x ph)))

Checked nominal proof certificate identified upstream as g_spsbc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfsbc1d (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_nfsbc1d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWsbc A x ps)))

Checked nominal proof certificate identified upstream as g_nfsbc1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfsbcd (ph ps : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (hyp_nfsbcd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_nfsbcd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))) (hyp_nfsbcd_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ps))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x (Compiler.CompactSourceSyntax.synWsbc A y ps)))

Checked nominal proof certificate identified upstream as g_nfsbcd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbcco (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_ph_y : y ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsbc A y (Compiler.CompactSourceSyntax.synWsbc (SemanticCore.Class.cv y) x ph)) (Compiler.CompactSourceSyntax.synWsbc A x ph))

Checked nominal proof certificate identified upstream as g_sbcco.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbc5 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsbc A x ph) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) ph)))

Checked nominal proof certificate identified upstream as g_sbc5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbc6g (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.synWsbc A x ph) (SemanticCore.Wff.all x ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp ph))))

Checked nominal proof certificate identified upstream as g_sbc6g.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sbciegft.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbciegf (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_sbciegf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ps)) (hyp_sbciegf_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsbc A x ph) ps))

Checked nominal proof certificate identified upstream as g_sbciegf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbcieg (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ps_x : x ∉ ps.fv) (hyp_sbcieg_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.synWsbc A x ph) ps))

Checked nominal proof certificate identified upstream as g_sbcieg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbciedf (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_sbcied_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A V))) (hyp_sbcied_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_sbciedf_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_sbciedf_4 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsbc A x ps) ch))

Checked nominal proof certificate identified upstream as g_sbciedf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqsbc1 (x : SemanticCore.Var) (A B V : SemanticCore.Class) (dv_B_x : x ∉ B.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsbc A x (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) B)) (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_eqsbc1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbcimg (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsbc A x (ph.imp ps)) ((Compiler.CompactSourceSyntax.synWsbc A x ph).imp (Compiler.CompactSourceSyntax.synWsbc A x ps))))

Checked nominal proof certificate identified upstream as g_sbcimg.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sbcan.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbceqal (x : SemanticCore.Var) (A B V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp ((SemanticCore.Wff.all x ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) B))).imp (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_sbceqal.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbeqalb (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A))) (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) B)))).imp (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_sbeqalb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbcbid (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_sbcbid_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_sbcbid_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsbc A x ps) (Compiler.CompactSourceSyntax.synWsbc A x ch)))

Checked nominal proof certificate identified upstream as g_sbcbid.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sbcbidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSbcbii (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_sbcbii_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ph ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWsbc A x ph) (Compiler.CompactSourceSyntax.synWsbc A x ps))

Checked nominal proof certificate identified upstream as g_sbcbii.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sbccomlem.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sbccom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRspesbca (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_B_x : x ∉ B.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A B) (Compiler.CompactSourceSyntax.synWsbc A x ph)).imp (Compiler.CompactSourceSyntax.synWrex x B ph))

Checked nominal proof certificate identified upstream as g_rspesbca.

Equations

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

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

Checked nominal proof certificate identified upstream as g_spesbc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCsbeq1 (x : SemanticCore.Var) (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsb A x C) (Compiler.CompactSourceSyntax.synCsb B x C)))

Checked nominal proof certificate identified upstream as g_csbeq1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCsbeq1d (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B C : SemanticCore.Class) (hyp_csbeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsb A x C) (Compiler.CompactSourceSyntax.synCsb B x C)))

Checked nominal proof certificate identified upstream as g_csbeq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCsbid (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsb (SemanticCore.Class.cv x) x A) A)

Checked nominal proof certificate identified upstream as g_csbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCsbeq1a (x : SemanticCore.Var) (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCsb A x B)))

Checked nominal proof certificate identified upstream as g_csbeq1a.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCsbeq2d (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B C : SemanticCore.Class) (hyp_csbeq2d_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_csbeq2d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsb A x B) (Compiler.CompactSourceSyntax.synCsb A x C)))

Checked nominal proof certificate identified upstream as g_csbeq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCsbeq2dv (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_ph_x : x ∉ ph.fv) (hyp_csbeq2dv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsb A x B) (Compiler.CompactSourceSyntax.synCsb A x C)))

Checked nominal proof certificate identified upstream as g_csbeq2dv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcsb1d (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfcsb1d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCsb A x B)))

Checked nominal proof certificate identified upstream as g_nfcsb1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcsb1 (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfcsb1_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCsb A x B))

Checked nominal proof certificate identified upstream as g_nfcsb1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nfcsb1v.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gNfcsb1v x A B dv_A_x = NFChoice.DirectNominalPrf.WPPReplay.gNfcsb1 x A B (NFChoice.DirectNominalPrf.WPPReplay.gNfcv x A ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcsbd (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfcsbd_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf y ph)) (hyp_nfcsbd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x A))) (hyp_nfcsbd_3 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCsb A y B)))

Checked nominal proof certificate identified upstream as g_nfcsbd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcsb (x y : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfcsb_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_nfcsb_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCsb A y B))

Checked nominal proof certificate identified upstream as g_nfcsb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCsbiebt (x : SemanticCore.Var) (A B C V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (Compiler.CompactSourceSyntax.synWnfc x C)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all x ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classEq B C))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsb A x B) C)))

Checked nominal proof certificate identified upstream as g_csbiebt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCsbiedf (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B C V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_csbiedf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_csbiedf_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x C))) (hyp_csbiedf_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A V))) (hyp_csbiedf_4 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)).imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsb A x B) C))

Checked nominal proof certificate identified upstream as g_csbiedf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCsbied (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B C V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_C_x : x ∉ C.fv) (dv_ph_x : x ∉ ph.fv) (hyp_csbied_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem A V))) (hyp_csbied_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A)).imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsb A x B) C))

Checked nominal proof certificate identified upstream as g_csbied.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElning (A B C V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCnin B C)) (Compiler.CompactSourceSyntax.synWnan (SemanticCore.Wff.classMem A B) (SemanticCore.Wff.classMem A C))))

Checked nominal proof certificate identified upstream as g_elning.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElcomplg (A B V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCcompl B)) (SemanticCore.Wff.classMem A B).neg))

Checked nominal proof certificate identified upstream as g_elcomplg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElin (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCin B C)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A B) (SemanticCore.Wff.classMem A C)))

Checked nominal proof certificate identified upstream as g_elin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElun (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCun B C)) (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classMem A B) (SemanticCore.Wff.classMem A C)))

Checked nominal proof certificate identified upstream as g_elun.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eldif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElsymdif (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCsymdif B C)) (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A B) (SemanticCore.Wff.classMem A C)).neg)

Checked nominal proof certificate identified upstream as g_elsymdif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElnin (A B C : SemanticCore.Class) (hyp_elbool_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCnin B C)) (Compiler.CompactSourceSyntax.synWnan (SemanticCore.Wff.classMem A B) (SemanticCore.Wff.classMem A C)))

Checked nominal proof certificate identified upstream as g_elnin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElcompl (A B : SemanticCore.Class) (hyp_elbool_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCcompl B)) (SemanticCore.Wff.classMem A B).neg)

Checked nominal proof certificate identified upstream as g_elcompl.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nincom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDblcompl (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCcompl A)) A)

Checked nominal proof certificate identified upstream as g_dblcompl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfnin (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfnin_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_nfnin_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCnin A B))

Checked nominal proof certificate identified upstream as g_nfnin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfcompl (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_nfbool_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCcompl A))

Checked nominal proof certificate identified upstream as g_nfcompl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfun (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_nfbool_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_nfbool_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCun A B))

Checked nominal proof certificate identified upstream as g_nfun.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nineq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nineq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_nineq12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNineq12i (A B C D : SemanticCore.Class) (hyp_nineqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_nineq12i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnin A C) (Compiler.CompactSourceSyntax.synCnin B D))

Checked nominal proof certificate identified upstream as g_nineq12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNineq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_nineqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnin C A) (Compiler.CompactSourceSyntax.synCnin C B)))

Checked nominal proof certificate identified upstream as g_nineq2d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_compleq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCompleqi (A B : SemanticCore.Class) (hyp_compleqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcompl A) (Compiler.CompactSourceSyntax.synCcompl B))

Checked nominal proof certificate identified upstream as g_compleqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gCompleqi A B hyp_compleqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_compleqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gCompleq A B)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCompleqd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_compleqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcompl A) (Compiler.CompactSourceSyntax.synCcompl B)))

Checked nominal proof certificate identified upstream as g_compleqd.

Equations

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

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

Checked nominal proof certificate identified upstream as g_difeq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_difeq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dfss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfss2 (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.synWss A B) (SemanticCore.Wff.all x ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B))))

Checked nominal proof certificate identified upstream as g_dfss2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfss3 (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.synWss A B) (Compiler.CompactSourceSyntax.synWral x A (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B)))

Checked nominal proof certificate identified upstream as g_dfss3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfss2f (x : SemanticCore.Var) (A B : SemanticCore.Class) (hyp_dfss2f_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_dfss2f_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A B) (SemanticCore.Wff.all x ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B))))

Checked nominal proof certificate identified upstream as g_dfss2f.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ssel.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ssel2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sseli.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSseli A B C hyp_sseli_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_sseli_1 (NFChoice.DirectNominalPrf.WPPReplay.gSsel A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSselii (A B C : SemanticCore.Class) (hyp_sseli_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)) (hyp_sselii_2 : Nominal.NPrf (SemanticCore.Wff.classMem C A)) : Nominal.NPrf (SemanticCore.Wff.classMem C B)

Checked nominal proof certificate identified upstream as g_sselii.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSselii A B C hyp_sseli_1 hyp_sselii_2 = NFChoice.DirectNominalPrf.Nominal.mp hyp_sselii_2 (NFChoice.DirectNominalPrf.WPPReplay.gSseli A B C hyp_sseli_1)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSseldi (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_sseli_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)) (hyp_sseldi_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem C A))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem C B))

Checked nominal proof certificate identified upstream as g_sseldi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSseld (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_sseld_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classMem C A).imp (SemanticCore.Wff.classMem C B)))

Checked nominal proof certificate identified upstream as g_sseld.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSselda (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_sseld_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem C A)).imp (SemanticCore.Wff.classMem C B))

Checked nominal proof certificate identified upstream as g_sselda.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSseldd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_sseld_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) (hyp_sseldd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem C A))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem C B))

Checked nominal proof certificate identified upstream as g_sseldd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsriv (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (hyp_ssriv_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)

Checked nominal proof certificate identified upstream as g_ssriv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsrdv (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ph_x : x ∉ ph.fv) (hyp_ssrdv_1 : Nominal.NPrf (ph.imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))

Checked nominal proof certificate identified upstream as g_ssrdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSstr2 (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp ((Compiler.CompactSourceSyntax.synWss B C).imp (Compiler.CompactSourceSyntax.synWss A C)))

Checked nominal proof certificate identified upstream as g_sstr2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sstr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSstri (A B C : SemanticCore.Class) (hyp_sstri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)) (hyp_sstri_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss B C)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A C)

Checked nominal proof certificate identified upstream as g_sstri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSstrd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_sstrd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) (hyp_sstrd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss B C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_sstrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5ss (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5ss_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)) (hyp_syl5ss_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss B C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_syl5ss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6ss (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl6ss_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) (hyp_syl6ss_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss B C)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_syl6ss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSylan9ss (ph ps : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_sylan9ss_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) (hyp_sylan9ss_2 : Nominal.NPrf (ps.imp (Compiler.CompactSourceSyntax.synWss B C))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_sylan9ss.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqssi (A B : SemanticCore.Class) (hyp_eqssi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)) (hyp_eqssi_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss B A)) : Nominal.NPrf (SemanticCore.Wff.classEq A B)

Checked nominal proof certificate identified upstream as g_eqssi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqssd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_eqssd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) (hyp_eqssd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss B A))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_eqssd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsid (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A A)

Checked nominal proof certificate identified upstream as g_ssid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsv (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ssv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sseq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sseq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sseq12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sseq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSseq1i A B C hyp_sseq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_sseq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gSseq1 A B C)

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

Checked nominal proof certificate identified upstream as g_sseq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSseq2i A B C hyp_sseq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_sseq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gSseq2 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSseq12i (A B C D : SemanticCore.Class) (hyp_sseq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_sseq12i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A C) (Compiler.CompactSourceSyntax.synWss B D))

Checked nominal proof certificate identified upstream as g_sseq12i.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sseq1d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sseq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSseq12d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_sseq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_sseq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A C) (Compiler.CompactSourceSyntax.synWss B D)))

Checked nominal proof certificate identified upstream as g_sseq12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqsstri (A B C : SemanticCore.Class) (hyp_eqsstr_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_eqsstr_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss B C)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A C)

Checked nominal proof certificate identified upstream as g_eqsstri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqsstr3i (A B C : SemanticCore.Class) (hyp_eqsstr3_1 : Nominal.NPrf (SemanticCore.Wff.classEq B A)) (hyp_eqsstr3_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss B C)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A C)

Checked nominal proof certificate identified upstream as g_eqsstr3i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSseqtri (A B C : SemanticCore.Class) (hyp_sseqtr_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)) (hyp_sseqtr_2 : Nominal.NPrf (SemanticCore.Wff.classEq B C)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A C)

Checked nominal proof certificate identified upstream as g_sseqtri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSseqtr4i (A B C : SemanticCore.Class) (hyp_sseqtr4_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)) (hyp_sseqtr4_2 : Nominal.NPrf (SemanticCore.Wff.classEq C B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A C)

Checked nominal proof certificate identified upstream as g_sseqtr4i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqsstrd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eqsstrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_eqsstrd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss B C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_eqsstrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqsstr3d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_eqsstr3d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B A))) (hyp_eqsstr3d_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss B C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_eqsstr3d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSseqtrd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_sseqtrd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) (hyp_sseqtrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_sseqtrd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSseqtr4d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_sseqtr4d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) (hyp_sseqtr4d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_sseqtr4d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3sstr4i (A B C D : SemanticCore.Class) (hyp_n_3sstr4_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)) (hyp_n_3sstr4_2 : Nominal.NPrf (SemanticCore.Wff.classEq C A)) (hyp_n_3sstr4_3 : Nominal.NPrf (SemanticCore.Wff.classEq D B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss C D)

Checked nominal proof certificate identified upstream as g_n_3sstr4i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3sstr4g (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_n_3sstr4g_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) (hyp_n_3sstr4g_2 : Nominal.NPrf (SemanticCore.Wff.classEq C A)) (hyp_n_3sstr4g_3 : Nominal.NPrf (SemanticCore.Wff.classEq D B)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss C D))

Checked nominal proof certificate identified upstream as g_n_3sstr4g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN3sstr4d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_n_3sstr4d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) (hyp_n_3sstr4d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C A))) (hyp_n_3sstr4d_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq D B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss C D))

Checked nominal proof certificate identified upstream as g_n_3sstr4d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5eqss (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5eqss_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_syl5eqss_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss B C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_syl5eqss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5eqssr (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5eqssr_1 : Nominal.NPrf (SemanticCore.Wff.classEq B A)) (hyp_syl5eqssr_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss B C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_syl5eqssr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6sseq (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl6sseq_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) (hyp_syl6sseq_2 : Nominal.NPrf (SemanticCore.Wff.classEq B C)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_syl6sseq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6sseqr (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl6ssr_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))) (hyp_syl6ssr_2 : Nominal.NPrf (SemanticCore.Wff.classEq C B)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_syl6sseqr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5sseq (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5sseq_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss B A)) (hyp_syl5sseq_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss B C))

Checked nominal proof certificate identified upstream as g_syl5sseq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl5sseqr (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl5sseqr_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss B A)) (hyp_syl5sseqr_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C A))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss B C))

Checked nominal proof certificate identified upstream as g_syl5sseqr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSyl6eqss (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_syl6eqss_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_syl6eqss_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss B C)) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))

Checked nominal proof certificate identified upstream as g_syl6eqss.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqimss.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eqimss2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqimssi (A B : SemanticCore.Class) (hyp_eqimssi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)

Checked nominal proof certificate identified upstream as g_eqimssi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gEqimssi A B hyp_eqimssi_1 = NFChoice.DirectNominalPrf.WPPReplay.gSseqtri A A B (NFChoice.DirectNominalPrf.WPPReplay.gSsid A) hyp_eqimssi_1

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNss (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.synWss A B).neg (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B).neg)))

Checked nominal proof certificate identified upstream as g_nss.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ss2ab.

Equations

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

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

Checked nominal proof certificate identified upstream as g_abss.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ssab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSs2abi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_ss2abi_1 : Nominal.NPrf (ph.imp ps)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cab x ph) (SemanticCore.Class.cab x ps))

Checked nominal proof certificate identified upstream as g_ss2abi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSs2abdv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (hyp_ss2abdv_1 : Nominal.NPrf (ph.imp (ps.imp ch))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cab x ps) (SemanticCore.Class.cab x ch)))

Checked nominal proof certificate identified upstream as g_ss2abdv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_abssdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAbssi (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (hyp_abssi_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cab x ph) A)

Checked nominal proof certificate identified upstream as g_abssi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ssab2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ssrab2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfpss2 (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWpss A B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss A B) (SemanticCore.Wff.classEq A B).neg))

Checked nominal proof certificate identified upstream as g_dfpss2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfpss3 (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWpss A B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss A B) (Compiler.CompactSourceSyntax.synWss B A).neg))

Checked nominal proof certificate identified upstream as g_dfpss3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPssss (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWpss A B).imp (Compiler.CompactSourceSyntax.synWss A B))

Checked nominal proof certificate identified upstream as g_pssss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPssssd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_pssssd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWpss A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A B))

Checked nominal proof certificate identified upstream as g_pssssd.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sspss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifeq1i (A B C : SemanticCore.Class) (hyp_difeq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif A C) (Compiler.CompactSourceSyntax.synCdif B C))

Checked nominal proof certificate identified upstream as g_difeq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gDifeq1i A B C hyp_difeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_difeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gDifeq1 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifeq2i (A B C : SemanticCore.Class) (hyp_difeq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif C A) (Compiler.CompactSourceSyntax.synCdif C B))

Checked nominal proof certificate identified upstream as g_difeq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gDifeq2i A B C hyp_difeq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_difeq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gDifeq2 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifeq1d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_difeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif A C) (Compiler.CompactSourceSyntax.synCdif B C)))

Checked nominal proof certificate identified upstream as g_difeq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifeq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_difeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif C A) (Compiler.CompactSourceSyntax.synCdif C B)))

Checked nominal proof certificate identified upstream as g_difeq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifeq12d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_difeq12d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_difeq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif A C) (Compiler.CompactSourceSyntax.synCdif B D)))

Checked nominal proof certificate identified upstream as g_difeq12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifeqri (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) (hyp_difeqri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B).neg) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif A B) C)

Checked nominal proof certificate identified upstream as g_difeqri.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eldifi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_eldifn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_difdif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifss (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdif A B) A)

Checked nominal proof certificate identified upstream as g_difss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDdif (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCvv A)) A)

Checked nominal proof certificate identified upstream as g_ddif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsdif (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdif A C) (Compiler.CompactSourceSyntax.synCdif B C)))

Checked nominal proof certificate identified upstream as g_ssdif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUneqri (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) (hyp_uneqri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A B) C)

Checked nominal proof certificate identified upstream as g_uneqri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnidm (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A A) A)

Checked nominal proof certificate identified upstream as g_unidm.

Equations

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

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

Checked nominal proof certificate identified upstream as g_uncom.

Equations

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

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

Checked nominal proof certificate identified upstream as g_uneq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_uneq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_uneq12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUneq1i (A B C : SemanticCore.Class) (hyp_uneq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A C) (Compiler.CompactSourceSyntax.synCun B C))

Checked nominal proof certificate identified upstream as g_uneq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gUneq1i A B C hyp_uneq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_uneq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gUneq1 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUneq2i (A B C : SemanticCore.Class) (hyp_uneq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun C A) (Compiler.CompactSourceSyntax.synCun C B))

Checked nominal proof certificate identified upstream as g_uneq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gUneq2i A B C hyp_uneq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_uneq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gUneq2 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUneq12i (A B C D : SemanticCore.Class) (hyp_uneq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_uneq12i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A C) (Compiler.CompactSourceSyntax.synCun B D))

Checked nominal proof certificate identified upstream as g_uneq12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUneq1d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_uneq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A C) (Compiler.CompactSourceSyntax.synCun B C)))

Checked nominal proof certificate identified upstream as g_uneq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUneq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_uneq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun C A) (Compiler.CompactSourceSyntax.synCun C B)))

Checked nominal proof certificate identified upstream as g_uneq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUneq12d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_uneq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_uneq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A C) (Compiler.CompactSourceSyntax.synCun B D)))

Checked nominal proof certificate identified upstream as g_uneq12d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_unass.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsun1 (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCun A B))

Checked nominal proof certificate identified upstream as g_ssun1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsun2 (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCun B A))

Checked nominal proof certificate identified upstream as g_ssun2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsun3 (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCun B C)))

Checked nominal proof certificate identified upstream as g_ssun3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elun1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elun2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnss1 (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCun A C) (Compiler.CompactSourceSyntax.synCun B C)))

Checked nominal proof certificate identified upstream as g_unss1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ssequn1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnss2 (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCun C A) (Compiler.CompactSourceSyntax.synCun C B)))

Checked nominal proof certificate identified upstream as g_unss2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnss12 (A B C D : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss A B) (Compiler.CompactSourceSyntax.synWss C D)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCun A C) (Compiler.CompactSourceSyntax.synCun B D)))

Checked nominal proof certificate identified upstream as g_unss12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ssequn2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnss (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss A C) (Compiler.CompactSourceSyntax.synWss B C)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCun A B) C))

Checked nominal proof certificate identified upstream as g_unss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnssi (A B C : SemanticCore.Class) (hyp_unssi_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A C)) (hyp_unssi_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss B C)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCun A B) C)

Checked nominal proof certificate identified upstream as g_unssi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnssd (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_unssd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss A C))) (hyp_unssd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss B C))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCun A B) C))

Checked nominal proof certificate identified upstream as g_unssd.

Equations

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

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

Checked nominal proof certificate identified upstream as g_rexun.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ralunb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElin2 (A B C X : SemanticCore.Class) (hyp_elin2_x : Nominal.NPrf (SemanticCore.Wff.classEq X (Compiler.CompactSourceSyntax.synCin B C))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A X) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A B) (SemanticCore.Wff.classMem A C)))

Checked nominal proof certificate identified upstream as g_elin2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_incom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIneqri (x : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) (hyp_ineqri_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) C)

Checked nominal proof certificate identified upstream as g_ineqri.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ineq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ineq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ineq12.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIneq1i (A B C : SemanticCore.Class) (hyp_ineq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A C) (Compiler.CompactSourceSyntax.synCin B C))

Checked nominal proof certificate identified upstream as g_ineq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gIneq1i A B C hyp_ineq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_ineq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gIneq1 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIneq2i (A B C : SemanticCore.Class) (hyp_ineq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin C A) (Compiler.CompactSourceSyntax.synCin C B))

Checked nominal proof certificate identified upstream as g_ineq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gIneq2i A B C hyp_ineq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_ineq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gIneq2 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIneq12i (A B C D : SemanticCore.Class) (hyp_ineq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_ineq12i_2 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A C) (Compiler.CompactSourceSyntax.synCin B D))

Checked nominal proof certificate identified upstream as g_ineq12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIneq1d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_ineq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A C) (Compiler.CompactSourceSyntax.synCin B C)))

Checked nominal proof certificate identified upstream as g_ineq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIneq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_ineq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin C A) (Compiler.CompactSourceSyntax.synCin C B)))

Checked nominal proof certificate identified upstream as g_ineq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIneq12d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_ineq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_ineq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A C) (Compiler.CompactSourceSyntax.synCin B D)))

Checked nominal proof certificate identified upstream as g_ineq12d.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dfss1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInidm (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A A) A)

Checked nominal proof certificate identified upstream as g_inidm.

Equations

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

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

Checked nominal proof certificate identified upstream as g_inass.

Equations

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

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

Checked nominal proof certificate identified upstream as g_in12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_in32.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIn4 (A B C D : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCin A B) (Compiler.CompactSourceSyntax.synCin C D)) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCin A C) (Compiler.CompactSourceSyntax.synCin B D)))

Checked nominal proof certificate identified upstream as g_in4.

Equations

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

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

Checked nominal proof certificate identified upstream as g_inindi.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sseqin2.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gSseqin2 A B = NFChoice.DirectNominalPrf.WPPReplay.gDfss1 A B

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInss1 (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCin A B) A)

Checked nominal proof certificate identified upstream as g_inss1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInss2 (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCin A B) B)

Checked nominal proof certificate identified upstream as g_inss2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsin (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss A B) (Compiler.CompactSourceSyntax.synWss A C)) (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCin B C)))

Checked nominal proof certificate identified upstream as g_ssin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsini (A B C : SemanticCore.Class) (hyp_ssini_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A B)) (hyp_ssini_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A C)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCin B C))

Checked nominal proof certificate identified upstream as g_ssini.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsrin (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCin A C) (Compiler.CompactSourceSyntax.synCin B C)))

Checked nominal proof certificate identified upstream as g_ssrin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSslin (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCin C A) (Compiler.CompactSourceSyntax.synCin C B)))

Checked nominal proof certificate identified upstream as g_sslin.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dfss4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfun2 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A B) (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCvv A) B)))

Checked nominal proof certificate identified upstream as g_dfun2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfin2 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) (Compiler.CompactSourceSyntax.synCdif A (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCvv B)))

Checked nominal proof certificate identified upstream as g_dfin2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifin (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif A (Compiler.CompactSourceSyntax.synCin A B)) (Compiler.CompactSourceSyntax.synCdif A B))

Checked nominal proof certificate identified upstream as g_difin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfun3 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A B) (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCvv A) (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCvv B))))

Checked nominal proof certificate identified upstream as g_dfun3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfin4 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) (Compiler.CompactSourceSyntax.synCdif A (Compiler.CompactSourceSyntax.synCdif A B)))

Checked nominal proof certificate identified upstream as g_dfin4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInvdif (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCvv B)) (Compiler.CompactSourceSyntax.synCdif A B))

Checked nominal proof certificate identified upstream as g_invdif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIndi (A B C : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A (Compiler.CompactSourceSyntax.synCun B C)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin A B) (Compiler.CompactSourceSyntax.synCin A C)))

Checked nominal proof certificate identified upstream as g_indi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUndi (A B C : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCin B C)) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCun A B) (Compiler.CompactSourceSyntax.synCun A C)))

Checked nominal proof certificate identified upstream as g_undi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIndir (A B C : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCun A B) C) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin A C) (Compiler.CompactSourceSyntax.synCin B C)))

Checked nominal proof certificate identified upstream as g_indir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUndir (A B C : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin A B) C) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCun A C) (Compiler.CompactSourceSyntax.synCun B C)))

Checked nominal proof certificate identified upstream as g_undir.

Equations

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