Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart007.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOtkelins3kg (A B C D T V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W) (SemanticCore.Wff.classMem C T)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synCopk B C)) (Compiler.CompactSourceSyntax.synCins3k D)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) D)))

Checked nominal proof certificate identified upstream as g_otkelins3kg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOtkelins2k (A B C D : SemanticCore.Class) (hyp_otkelinsk_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_otkelinsk_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_otkelinsk_3 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synCopk B C)) (Compiler.CompactSourceSyntax.synCins2k D)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A C) D))

Checked nominal proof certificate identified upstream as g_otkelins2k.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOtkelins3k (A B C D : SemanticCore.Class) (hyp_otkelinsk_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_otkelinsk_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_otkelinsk_3 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synCopk B C)) (Compiler.CompactSourceSyntax.synCins3k D)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) D))

Checked nominal proof certificate identified upstream as g_otkelins3k.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimakg (y : SemanticCore.Var) (A B C V : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_C_y : y ∉ C.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem C V).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCimak A B)) (Compiler.CompactSourceSyntax.synWrex y B (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) C) A))))

Checked nominal proof certificate identified upstream as g_elimakg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimakvg (y : SemanticCore.Var) (A C V : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_C_y : y ∉ C.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem C V).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCimak A Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWex y (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) C) A))))

Checked nominal proof certificate identified upstream as g_elimakvg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimak (y : SemanticCore.Var) (A B C : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_C_y : y ∉ C.fv) (hyp_elimak_1 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCimak A B)) (Compiler.CompactSourceSyntax.synWrex y B (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) C) A)))

Checked nominal proof certificate identified upstream as g_elimak.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimakv (y : SemanticCore.Var) (A C : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_C_y : y ∉ C.fv) (hyp_elimak_1 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCimak A Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWex y (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) C) A)))

Checked nominal proof certificate identified upstream as g_elimakv.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart008.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelcokg (x : SemanticCore.Var) (A B C D V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCcomk C D)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A (SemanticCore.Class.cv x)) D) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) B) C)))))

Checked nominal proof certificate identified upstream as g_opkelcokg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelcok (x : SemanticCore.Var) (A B C D : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) (hyp_opkelcok_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opkelcok_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCcomk C D)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A (SemanticCore.Class.cv x)) D) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) B) C))))

Checked nominal proof certificate identified upstream as g_opkelcok.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElp6 (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.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCp6 B)) (SemanticCore.Wff.all x (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCsn A)) B))))

Checked nominal proof certificate identified upstream as g_elp6.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart009.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelsikg (x y : SemanticCore.Var) (A B C V W : 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) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCsik C)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) C))))))

Checked nominal proof certificate identified upstream as g_opkelsikg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpksnelsik (A B C : SemanticCore.Class) (hyp_opksnelsik_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opksnelsik_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synCsik C)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) C))

Checked nominal proof certificate identified upstream as g_opksnelsik.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sikssvvk.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart010.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSikss1c1c (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCsik A) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synC1c Compiler.CompactSourceSyntax.synC1c))

Checked nominal proof certificate identified upstream as g_sikss1c1c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelssetkg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synWss A B)))

Checked nominal proof certificate identified upstream as g_opkelssetkg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElssetkg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn A) B) Compiler.CompactSourceSyntax.synCssetk) (SemanticCore.Wff.classMem A B)))

Checked nominal proof certificate identified upstream as g_elssetkg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElssetk (A B : SemanticCore.Class) (hyp_elssetk_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_elssetk_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn A) B) Compiler.CompactSourceSyntax.synCssetk) (SemanticCore.Wff.classMem A B))

Checked nominal proof certificate identified upstream as g_elssetk.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart011.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelimagekg (A B C V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCimagek C)) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCimak C A))))

Checked nominal proof certificate identified upstream as g_opkelimagekg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelimagek (A B C : SemanticCore.Class) (hyp_opkelimagek_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_opkelimagek_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCimagek C)) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCimak C A)))

Checked nominal proof certificate identified upstream as g_opkelimagek.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpkelidkg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synCidk) (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_opkelidkg.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnvkssvvk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvkxpk (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCxpk A B)) (Compiler.CompactSourceSyntax.synCxpk B A))

Checked nominal proof certificate identified upstream as g_cnvkxpk.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart012.

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

Checked nominal proof certificate identified upstream as g_inxpk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsetkssvvk : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Compiler.CompactSourceSyntax.synCssetk (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_ssetkssvvk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIns2kss (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCins2k A) (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_ins2kss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIns3kss (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCins3k A) (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_ins3kss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIdkssvvk : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Compiler.CompactSourceSyntax.synCidk (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_idkssvvk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimaksn (A B C : SemanticCore.Class) (hyp_elimaksn_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_elimaksn_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCimak A (Compiler.CompactSourceSyntax.synCsn B))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B C) A))

Checked nominal proof certificate identified upstream as g_elimaksn.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart013.

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

Checked nominal proof certificate identified upstream as g_xpkvexg.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cnvkexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvkex (A : SemanticCore.Class) (hyp_cnvkex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCcnvk A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_cnvkex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpkexg (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.synCxpk A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_xpkexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpkex (A B : SemanticCore.Class) (hyp_xpkex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_xpkex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCxpk A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_xpkex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_p6exg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfuni12 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni1 A) (Compiler.CompactSourceSyntax.synCp6 (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv A)))

Checked nominal proof certificate identified upstream as g_dfuni12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_uni1exg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUni1ex (A : SemanticCore.Class) (hyp_uni1ex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni1 A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_uni1ex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ssetkex.

Equations

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