Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part026.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSifrndv (D R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsi R) Compiler.CompactSourceSyntax.synCfound (Compiler.CompactSourceSyntax.synCpw1 D)))

Checked nominal proof certificate identified upstream as g_sifrndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part027.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSiwendv (D R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsi R) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synCpw1 D)))

Checked nominal proof certificate identified upstream as g_siwendv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardtypedleastndv (y z : SemanticCore.Var) (D R K : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_q : q ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_D_z : z ∉ D.fv) (dv_K_q : q ∉ K.fv) (dv_K_y : y ∉ K.fv) (dv_K_z : z ∉ K.fv) (dv_R_q : q ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_q_y : q ≠ y) (dv_q_z : q ≠ z) (dv_y_z : y ≠ z) (hyp_wecutcardtypedleastndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutcardtypedleastndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem K Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))) K)).imp (Compiler.CompactSourceSyntax.synWrex y (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv y))))))) K) (Compiler.CompactSourceSyntax.synWral z (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv z))))))) K).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCsi R)) (SemanticCore.Class.cv z)))))))

Checked nominal proof certificate identified upstream as g_wecutcardtypedleastndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutssndv (x y : SemanticCore.Var) (D R : SemanticCore.Class) (_dv_D_x : x ∉ D.fv) (_dv_D_y : y ∉ D.fv) (_dv_R_x : x ∉ R.fv) (_dv_R_y : y ∉ R.fv) (_dv_x_y : x ≠ y) (hyp_wecutssndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_wecutssndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutnclecndv (x y : SemanticCore.Var) (D R : SemanticCore.Class) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_x_y : x ≠ y) (hyp_wecutnclecndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))))

Checked nominal proof certificate identified upstream as g_wecutnclecndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part028.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutnclecclndv (A B D R : SemanticCore.Class) (_dv_A_R : Disjoint A.fv R.fv) (hyp_wecutnclecclndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)).imp ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A D) (SemanticCore.Wff.classMem B D) (Compiler.CompactSourceSyntax.synWbr A R B)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn A)))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn B)))))))

Checked nominal proof certificate identified upstream as g_wecutnclecclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecuttypedbrndv (y z : SemanticCore.Var) (D R : SemanticCore.Class) (_dv_D_y : y ∉ D.fv) (_dv_D_z : z ∉ D.fv) (_dv_R_y : y ∉ R.fv) (_dv_R_z : z ∉ R.fv) (_dv_y_z : y ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCsi R)) (SemanticCore.Class.cv z)) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv y))) R (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv z))))))

Checked nominal proof certificate identified upstream as g_wecuttypedbrndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecuttypednclecndv (y z : SemanticCore.Var) (D R : SemanticCore.Class) (dv_D_y : y ∉ D.fv) (dv_D_z : z ∉ D.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_y_z : y ≠ z) (hyp_wecuttypednclecndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)))).imp ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCsi R)) (SemanticCore.Class.cv z)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv y))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv z))))))))))

Checked nominal proof certificate identified upstream as g_wecuttypednclecndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardtypedcardleastndv (y z : SemanticCore.Var) (D R K : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_q : q ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_D_z : z ∉ D.fv) (dv_K_q : q ∉ K.fv) (dv_K_y : y ∉ K.fv) (dv_K_z : z ∉ K.fv) (dv_R_q : q ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_q_y : q ≠ y) (dv_q_z : q ≠ z) (dv_y_z : y ≠ z) (hyp_wecutcardtypedcardleastndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutcardtypedcardleastndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem K Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))) K)).imp (Compiler.CompactSourceSyntax.synWrex y (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv y))))))) K) (Compiler.CompactSourceSyntax.synWral z (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv z))))))) K).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv y))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv z)))))))))))))

Checked nominal proof certificate identified upstream as g_wecutcardtypedcardleastndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElwppcandstrictslice (C : SemanticCore.Class) (k : SemanticCore.Var) (F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C)))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCwppcand F C)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCltc C)))

Checked nominal proof certificate identified upstream as g_elwppcandstrictslice.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachexndv (C F : SemanticCore.Class) (hyp_wppreachexndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppreach F C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppreachexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandexndv (C F : SemanticCore.Class) (hyp_wppcandexndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppcand F C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppcandexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandstrictsliceexndv (C F : SemanticCore.Class) (hyp_wppcandstrictsliceexndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppcandstrictsliceexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandnltpivoteqd (C : SemanticCore.Class) (k : SemanticCore.Var) (F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCwppcand F C)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCltc C).neg).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv k) C))

Checked nominal proof certificate identified upstream as g_wppcandnltpivoteqd.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part029.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutcardrepleastdndv (y : SemanticCore.Var) (D R : SemanticCore.Class) (k : SemanticCore.Var) (K : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_k : k ∉ D.fv) (dv_D_q : q ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_K_k : k ∉ K.fv) (dv_K_q : q ∉ K.fv) (dv_K_y : y ∉ K.fv) (dv_R_k : k ∉ R.fv) (dv_R_q : q ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_k_q : k ≠ q) (dv_k_y : k ≠ y) (dv_q_y : q ≠ y) (hyp_wecutcardrepleastdndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutcardrepleastdndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem K Compiler.CompactSourceSyntax.synCvv)) (hyp_wecutcardrepleastdndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral k K (Compiler.CompactSourceSyntax.synWrex q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))))))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWne K Compiler.CompactSourceSyntax.synC0).imp (Compiler.CompactSourceSyntax.synWrex y (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv y))))))) K) (Compiler.CompactSourceSyntax.synWral k K (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv y))))))) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k))))))

Checked nominal proof certificate identified upstream as g_wecutcardrepleastdndv.

Equations

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