Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part015.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelrescnvfunndv (A B : SemanticCore.Class) (_hyp_wppqkrelrescnvfunndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (_hyp_wppqkrelrescnvfunndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synCwppqkrelkernel) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCxp A B))))))

Checked nominal proof certificate identified upstream as g_wppqkrelrescnvfunndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part016.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelrestypedenqkndv (A B : SemanticCore.Class) (hyp_wppqkrelresf1oqkndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_wppqkrelresf1oqkndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCxp A B))) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCqkrel (Compiler.CompactSourceSyntax.synCxp A B)))

Checked nominal proof certificate identified upstream as g_wppqkrelrestypedenqkndv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_wppqkrelxprebasendv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelrestypedenndv (A B : SemanticCore.Class) (hyp_wppqkrelresf1ondv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_wppqkrelresf1ondv_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCxp A B))) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCxpk A B))

Checked nominal proof certificate identified upstream as g_wppqkrelrestypedenndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardmonodndv (A D : SemanticCore.Class) (hyp_hncardmonodndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hncardmonodndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss D A).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard D) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synChncard A)))

Checked nominal proof certificate identified upstream as g_hncardmonodndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardf1leimpndv (A D F : SemanticCore.Class) (hyp_hncardf1leimpndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (_hyp_hncardf1leimpndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hncardf1leimpndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 F D A).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard D) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synChncard A)))

Checked nominal proof certificate identified upstream as g_hncardf1leimpndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardnclecndv (A D : SemanticCore.Class) (hyp_hncardnclecndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hncardnclecndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc D) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc A)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard D) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synChncard A)))

Checked nominal proof certificate identified upstream as g_hncardnclecndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnordcardnclecndv (A D : SemanticCore.Class) (hyp_hnordcardnclecndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hnordcardnclecndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc D) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc A)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synChnord D)) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synChnord A))))

Checked nominal proof certificate identified upstream as g_hnordcardnclecndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelliteralenndv (X : SemanticCore.Class) (hyp_wppqkrelliteralenndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxpk X X) Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCxp X X))) Compiler.CompactSourceSyntax.synCnnc))

Checked nominal proof certificate identified upstream as g_wppqkrelliteralenndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppqkrelliteralnceqndv (X : SemanticCore.Class) (hyp_wppqkrelliteralnceqndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxpk X X) Compiler.CompactSourceSyntax.synCnnc)) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCxp X X))) Compiler.CompactSourceSyntax.synCnnc)))

Checked nominal proof certificate identified upstream as g_wppqkrelliteralnceqndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnordlnquoeq (A R : SemanticCore.Class) (_dv_A_R : Disjoint A.fv R.fv) (hyp_hnordlnquoeq_1 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synClnker R) (Compiler.CompactSourceSyntax.synChwniso A))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synClnquo R (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synChnord A))

Checked nominal proof certificate identified upstream as g_hnordlnquoeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnordwefromcmp (A R : SemanticCore.Class) (dv_A_R : Disjoint A.fv R.fv) (hyp_hnordwefromcmp_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_hnordwefromcmp_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_hnordwefromcmp_3 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop R (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synClnpwc (Compiler.CompactSourceSyntax.synChwcn A)))) (hyp_hnordwefromcmp_4 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synClnker R) (Compiler.CompactSourceSyntax.synChwniso A))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synClnqord R (Compiler.CompactSourceSyntax.synChwcn A)) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synChnord A))

Checked nominal proof certificate identified upstream as g_hnordwefromcmp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutfnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synChncodecutfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hncodecutfnfn.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part017.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutpairfnfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synChncodecutpairfn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hncodecutpairfnfn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hncodecutpairfnex.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part018.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutfnval (x : SemanticCore.Var) (D R : SemanticCore.Class) (hyp_hncodecutfnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_hncodecutfnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synChncodecutfn (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop R D) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)))

Checked nominal proof certificate identified upstream as g_hncodecutfnval.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part019.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutpairfnval (x : SemanticCore.Var) (D R : SemanticCore.Class) (hyp_hncodecutpairfnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_hncodecutpairfnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synChncodecutpairfn (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop R D) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCop R D)))

Checked nominal proof certificate identified upstream as g_hncodecutpairfnval.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hncodecmpsetexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrhncodecmpset (x v u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_u_x : u ≠ x) (dv_v_x : v ≠ x) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChncodecmpset A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synChncodecutrel A) (SemanticCore.Class.cv v))))))

Checked nominal proof certificate identified upstream as g_brhncodecmpset.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutinputmemi (x : SemanticCore.Var) (A D R : SemanticCore.Class) (_dv_A_R : Disjoint A.fv R.fv) (hyp_hncodecutinputmemi_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_hncodecutinputmemi_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop R D) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop R D) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synChncodecutinputs A)))

Checked nominal proof certificate identified upstream as g_hncodecutinputmemi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutreledgei (x : SemanticCore.Var) (A D R : SemanticCore.Class) (dv_A_R : Disjoint A.fv R.fv) (hyp_hncodecutreledgei_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_hncodecutreledgei_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop R D) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChncodecutrel A) (Compiler.CompactSourceSyntax.synCop R D)))

Checked nominal proof certificate identified upstream as g_hncodecutreledgei.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnpwquoinputfnvalhwcn (u : SemanticCore.Var) (A : SemanticCore.Class) (_dv_A_u : u ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synClnpwquoinputfn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))

Checked nominal proof certificate identified upstream as g_lnpwquoinputfnvalhwcn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodeinputproductdecode (x u : SemanticCore.Var) (D : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_x : x ∉ D.fv) (dv_p_x : p ≠ x) (dv_u_x : u ≠ x) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCpw1 D))).imp (Compiler.CompactSourceSyntax.synWrex x D (SemanticCore.Wff.classEq (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_hncodeinputproductdecode.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part020.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutinputdecode (x u : SemanticCore.Var) (A : SemanticCore.Class) (p : SemanticCore.Var) (_dv_A_p : p ∉ A.fv) (dv_A_u : u ∉ A.fv) (_dv_A_x : x ∉ A.fv) (dv_p_u : p ≠ u) (dv_p_x : p ≠ x) (dv_u_x : u ≠ x) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synChncodecutinputs A)).imp (Compiler.CompactSourceSyntax.synWrex u (Compiler.CompactSourceSyntax.synChwcn A) (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))))

Checked nominal proof certificate identified upstream as g_hncodecutinputdecode.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecutpairfnvalhwcn (x u : SemanticCore.Var) (A : SemanticCore.Class) (_dv_A_u : u ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synChncodecutpairfn (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (SemanticCore.Class.cv x)) (SemanticCore.Class.cv u))))

Checked nominal proof certificate identified upstream as g_hncodecutpairfnvalhwcn.

Equations

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