Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk014Compact001Part035.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwtrnbrd (x y f r : SemanticCore.Var) (_dv_f_x : f ≠ x) (_dv_f_y : f ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv x)) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_hwtrnbrd.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part036.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwtrnisob (f r : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))))

Checked nominal proof certificate identified upstream as g_hwtrnisob.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part037.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsotargettransport (A B S : SemanticCore.Class) (f r : SemanticCore.Var) (_dv_A_f : f ∉ A.fv) (_dv_B_f : f ∉ B.fv) (_dv_S_f : f ∉ S.fv) (_dv_f_r : f ≠ r) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) (SemanticCore.Class.cv r) S A B) (Compiler.CompactSourceSyntax.synWss S (Compiler.CompactSourceSyntax.synCxp B B))).imp (SemanticCore.Wff.classEq S (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))))

Checked nominal proof certificate identified upstream as g_isotargettransport.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwnisogeniso (v u : SemanticCore.Var) (A : SemanticCore.Class) (f r : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_A_r : r ∉ A.fv) (dv_f_r : f ≠ r) (dv_f_u : f ≠ u) (dv_f_v : f ≠ v) (dv_r_u : r ≠ u) (dv_r_v : r ≠ v) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A))) (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWrex r Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Class.cv u)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (SemanticCore.Class.cv v))))))))

Checked nominal proof certificate identified upstream as g_elhwnisogeniso.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcnraw (u : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcodes A)))

Checked nominal proof certificate identified upstream as g_hwcnraw.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcnsupp (u : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))

Checked nominal proof certificate identified upstream as g_hwcnsupp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcnpair (u : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))

Checked nominal proof certificate identified upstream as g_hwcnpair.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part038.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisorawgeni (v u : SemanticCore.Var) (A : SemanticCore.Class) (f r : SemanticCore.Var) (_dv_A_f : f ∉ A.fv) (dv_A_r : r ∉ A.fv) (dv_f_r : f ≠ r) (dv_f_u : f ≠ u) (dv_f_v : f ≠ v) (dv_r_u : r ≠ u) (dv_r_v : r ≠ v) (_dv_u_v : u ≠ v) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A))) (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)))).imp (Compiler.CompactSourceSyntax.synWrex r Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Class.cv u)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (SemanticCore.Class.cv v))))))

Checked nominal proof certificate identified upstream as g_hwnisorawgeni.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part039.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisogenrawi (v u : SemanticCore.Var) (A : SemanticCore.Class) (f r : SemanticCore.Var) (_dv_A_f : f ∉ A.fv) (_dv_A_r : r ∉ A.fv) (_dv_f_r : f ≠ r) (_dv_f_u : f ≠ u) (_dv_f_v : f ≠ v) (_dv_r_u : r ≠ u) (_dv_r_v : r ≠ v) (_dv_u_v : u ≠ v) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Class.cv u)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (SemanticCore.Class.cv v))))).imp (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))))

Checked nominal proof certificate identified upstream as g_hwnisogenrawi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisowitnessb (v u : SemanticCore.Var) (A : SemanticCore.Class) (f r : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_A_r : r ∉ A.fv) (dv_f_r : f ≠ r) (dv_f_u : f ≠ u) (dv_f_v : f ≠ v) (dv_r_u : r ≠ u) (dv_r_v : r ≠ v) (dv_u_v : u ≠ v) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWrex r Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (SemanticCore.Class.cv u)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (SemanticCore.Class.cv v)))))) (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))))))

Checked nominal proof certificate identified upstream as g_hwnisowitnessb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisohwisob (v u : SemanticCore.Var) (A : SemanticCore.Class) (dv_u_v : u ≠ v) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwiso A) (SemanticCore.Class.cv v))))

Checked nominal proof certificate identified upstream as g_hwnisohwisob.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hwcnexg.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hwnisoexg.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part040.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisosymi (v u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_u_v : u ≠ v) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv u)))

Checked nominal proof certificate identified upstream as g_hwnisosymi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisotri (w v u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_A_w : w ∉ A.fv) (dv_u_v : u ≠ v) (dv_u_w : u ≠ w) (dv_v_w : v ≠ w) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv w))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv w)))

Checked nominal proof certificate identified upstream as g_hwnisotri.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisoer (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChwniso A) Compiler.CompactSourceSyntax.synCer (Compiler.CompactSourceSyntax.synChwcn A)))

Checked nominal proof certificate identified upstream as g_hwnisoer.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisorefli (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 (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv u)))

Checked nominal proof certificate identified upstream as g_hwnisorefli.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisoerv (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChwniso A) Compiler.CompactSourceSyntax.synCer Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_hwnisoerv.

Equations

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