Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart014.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSikexlem (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) (hyp_sikexlem_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synC1c Compiler.CompactSourceSyntax.synC1c))) (hyp_sikexlem_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss B (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synC1c Compiler.CompactSourceSyntax.synC1c))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.all x (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))) A) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))) B)))))

Checked nominal proof certificate identified upstream as g_sikexlem.

Equations

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

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

Checked nominal proof certificate identified upstream as g_sikexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSikex (A : SemanticCore.Class) (hyp_sikex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsik A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_sikex.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart015.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfimak2 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCimak A B) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCp6 (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synC1c Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCin A (Compiler.CompactSourceSyntax.synCxpk B Compiler.CompactSourceSyntax.synCvv))))))))

Checked nominal proof certificate identified upstream as g_dfimak2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_imakexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImakex (A B : SemanticCore.Class) (hyp_imakex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_imakex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCimak A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_imakex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfpw12 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpw1 A) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCxpk A A)) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_dfpw12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pw1exg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1ex (A : SemanticCore.Class) (hyp_pw1ex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_pw1ex.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart016.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInsklem (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_B_z : z ∉ B.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_insklem_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)))) (hyp_insklem_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss B (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.all x (SemanticCore.Wff.all y (SemanticCore.Wff.all z (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))) A) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv y) (SemanticCore.Class.cv z))) B))))))

Checked nominal proof certificate identified upstream as g_insklem.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart017.

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

Checked nominal proof certificate identified upstream as g_ins2kexg.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ins3kexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIns2kex (A : SemanticCore.Class) (hyp_inskex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCins2k A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ins2kex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIns3kex (A : SemanticCore.Class) (hyp_inskex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCins3k A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ins3kex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_cokexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCokex (A B : SemanticCore.Class) (hyp_cokex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_cokex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCcomk A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_cokex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_imagekexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImagekex (A : SemanticCore.Class) (hyp_imagekex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCimagek A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_imagekex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfidk2 : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCidk (Compiler.CompactSourceSyntax.synCin Compiler.CompactSourceSyntax.synCssetk (Compiler.CompactSourceSyntax.synCcnvk Compiler.CompactSourceSyntax.synCssetk)))

Checked nominal proof certificate identified upstream as g_dfidk2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_idkex.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart018.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfuni3 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni A) (Compiler.CompactSourceSyntax.synCuni1 (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCcnvk Compiler.CompactSourceSyntax.synCssetk) A)))

Checked nominal proof certificate identified upstream as g_dfuni3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_uniexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUniex (A : SemanticCore.Class) (hyp_uniex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_uniex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfint3 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCint A) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCuni1 (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCssetk)) A))))

Checked nominal proof certificate identified upstream as g_dfint3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_intexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIntex (A : SemanticCore.Class) (hyp_intex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCint A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_intex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSetswith (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (SemanticCore.Class.cab x (SemanticCore.Wff.classMem A (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synCimak Compiler.CompactSourceSyntax.synCssetk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn A))) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_setswith.

Equations

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

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

Checked nominal proof certificate identified upstream as g_setswithex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNdisjrelk (A B : SemanticCore.Class) (hyp_ndisjrelk_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_ndisjrelk_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.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.synWne (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_ndisjrelk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAbexv (ph : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab x ph) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_abexv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnipw1 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCpw1 A)) A)

Checked nominal proof certificate identified upstream as g_unipw1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pw1exb.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart019.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfpw2 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpw A) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCssetk (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCpw1 A) Compiler.CompactSourceSyntax.synCvv)) Compiler.CompactSourceSyntax.synC1c)))

Checked nominal proof certificate identified upstream as g_dfpw2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_pwexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPwex (A : SemanticCore.Class) (hyp_pwex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_pwex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqpw1uni (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A Compiler.CompactSourceSyntax.synC1c).imp (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))))

Checked nominal proof certificate identified upstream as g_eqpw1uni.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1equn (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_pw1equn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_pw1equn_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 B)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv x))) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv y)))))))

Checked nominal proof certificate identified upstream as g_pw1equn.

Equations

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