Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart020.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1eqadj (x y : SemanticCore.Var) (A B C : 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_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_x_y : x ≠ y) (hyp_pw1eqadj_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_pw1eqadj_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpw1 C) (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCsn B))) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv x))) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))))

Checked nominal proof certificate identified upstream as g_pw1eqadj.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sspw1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfiota2 (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_ph_y : y ∉ ph.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCio x ph) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cab y (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb ph (SemanticCore.Wff.objEq x y))))))

Checked nominal proof certificate identified upstream as g_dfiota2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNfiota1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x (Compiler.CompactSourceSyntax.synCio x ph))

Checked nominal proof certificate identified upstream as g_nfiota1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIotabi (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb ph ps)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCio x ph) (Compiler.CompactSourceSyntax.synCio x ps)))

Checked nominal proof certificate identified upstream as g_iotabi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUniabio (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf ((SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb ph (SemanticCore.Wff.objEq x y))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cab x ph)) (SemanticCore.Class.cv y)))

Checked nominal proof certificate identified upstream as g_uniabio.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIotaval (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf ((SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWb ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCio x ph) (SemanticCore.Class.cv y)))

Checked nominal proof certificate identified upstream as g_iotaval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIota1 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWeu x ph).imp (Compiler.CompactSourceSyntax.synWb ph (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCio x ph) (SemanticCore.Class.cv x))))

Checked nominal proof certificate identified upstream as g_iota1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIotanul (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWeu x ph).neg.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCio x ph) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_iotanul.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIotaex (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCio x ph) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_iotaex.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart021.

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

Checked nominal proof certificate identified upstream as g_iota4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIotabidv (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) (hyp_iotabidv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCio x ps) (Compiler.CompactSourceSyntax.synCio x ch)))

Checked nominal proof certificate identified upstream as g_iotabidv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIotacl (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWeu x ph).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCio x ph) (SemanticCore.Class.cab x ph)))

Checked nominal proof certificate identified upstream as g_iotacl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReiotacl2 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWreu x A ph).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCio x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph)) (Compiler.CompactSourceSyntax.synCrab x A ph)))

Checked nominal proof certificate identified upstream as g_reiotacl2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gReiotacl (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWreu x A ph).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCio x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph)) A))

Checked nominal proof certificate identified upstream as g_reiotacl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIota2df (ph ps ch : SemanticCore.Wff) (x : SemanticCore.Var) (B V : SemanticCore.Class) (hyp_iota2df_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem B V))) (hyp_iota2df_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWeu x ps))) (hyp_iota2df_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) B)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_iota2df_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf x ph)) (hyp_iota2df_5 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnf x ch))) (hyp_iota2df_6 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWnfc x B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ch (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCio x ps) B)))

Checked nominal proof certificate identified upstream as g_iota2df.

Equations

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

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

Checked nominal proof certificate identified upstream as g_iota2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_reiota2.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart022.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfaddc2 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc A B) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 B))) A))

Checked nominal proof certificate identified upstream as g_dfaddc2.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart023.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddcexlem : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_addcexlem.

Equations

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

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

Checked nominal proof certificate identified upstream as g_addceq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_addceq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_addceq12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_addceq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAddceq1i A B C hyp_addceqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_addceqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gAddceq1 A B C)

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

Checked nominal proof certificate identified upstream as g_addceq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gAddceq2i A B C hyp_addceqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_addceqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gAddceq2 A B C)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddceq12i (A B C D : SemanticCore.Class) (hyp_addceqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) (hyp_addceqi_2 : Nominal.NPrf (SemanticCore.Wff.classEq C D)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc A C) (Compiler.CompactSourceSyntax.synCplc B D))

Checked nominal proof certificate identified upstream as g_addceq12i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddceq1d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_addceqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc A C) (Compiler.CompactSourceSyntax.synCplc B C)))

Checked nominal proof certificate identified upstream as g_addceq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddceq2d (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_addceqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc C A) (Compiler.CompactSourceSyntax.synCplc C B)))

Checked nominal proof certificate identified upstream as g_addceq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddceq12d (ph : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_addceqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_addceqd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc A C) (Compiler.CompactSourceSyntax.synCplc B D)))

Checked nominal proof certificate identified upstream as g_addceq12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0cex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0c Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_n_0cex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddcexg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_addcexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddcex (A B : SemanticCore.Class) (hyp_addcex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_addcex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_addcex.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart024.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfnnc2 (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synCint (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cab x (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0c (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCssetk (Compiler.CompactSourceSyntax.synCcomk Compiler.CompactSourceSyntax.synCssetk (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))) Compiler.CompactSourceSyntax.synC1c))))

Checked nominal proof certificate identified upstream as g_dfnnc2.

Equations

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