Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part084.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHninjraisedselfcutcmpndv (x u : SemanticCore.Var) (A : SemanticCore.Class) (f : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_A_u : u ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_f_u : f ≠ u) (dv_f_x : f ≠ x) (dv_u_x : u ≠ x) (hyp_hninjraisedselfcutcmpndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synChnord A) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))).imp (Compiler.CompactSourceSyntax.synWrex u (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))) (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))) (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))))))

Checked nominal proof certificate identified upstream as g_hninjraisedselfcutcmpndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnselfcutnoex2ndv (x u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_u_x : u ≠ x) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWrex u (Compiler.CompactSourceSyntax.synChwcn A) (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (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))))).neg

Checked nominal proof certificate identified upstream as g_hnselfcutnoex2ndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardtc2nodomndv (A : SemanticCore.Class) (hyp_hncardtc2nodomndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard A) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc A)))).neg

Checked nominal proof certificate identified upstream as g_hncardtc2nodomndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6representedmonondv (X Y : SemanticCore.Class) (hyp_wppconcrete6representedmonondv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (hyp_wppconcrete6representedmonondv_2 : Nominal.NPrf (SemanticCore.Wff.classMem Y Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc X))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc Y)))))))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc X)))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc Y))))))))))

Checked nominal proof certificate identified upstream as g_wppconcrete6representedmonondv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLetc6ncrepdv (z : SemanticCore.Var) (M N : SemanticCore.Class) (dv_M_z : z ∉ M.fv) (dv_N_z : z ∉ N.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc N)))))))).imp (Compiler.CompactSourceSyntax.synWex z (SemanticCore.Wff.classEq M (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc (SemanticCore.Class.cv z)))))))))))

Checked nominal proof certificate identified upstream as g_letc6ncrepdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6tcvalncndv : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))))) Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_wppconcrete6tcvalncndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part085.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6tcbandgrowthfrompointhwclecdndv (y : SemanticCore.Var) (hyp_wppconcrete6tcbandgrowthfrompointhwclecdndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWwpp.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))))))) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)).imp ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))).imp (Compiler.CompactSourceSyntax.synWwpp.imp ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6fn (SemanticCore.Class.cv y)))))))

Checked nominal proof certificate identified upstream as g_wppconcrete6tcbandgrowthfrompointhwclecdndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part086.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6stoppedgrowthfrompointndv (y : SemanticCore.Var) (hyp_wppconcrete6stoppedgrowthfrompointndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWwpp.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWwpp.imp (Compiler.CompactSourceSyntax.synWral y (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCwppstopstep Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))))) ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))) (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_wppconcrete6stoppedgrowthfrompointndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6notwppfrompointndv (hyp_wppconcrete6notwppfrompointndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWwpp.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c))))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppconcrete6fn (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard Compiler.CompactSourceSyntax.synC1c)))))))))))) : Nominal.NPrf Compiler.CompactSourceSyntax.synWwpp.neg

Checked nominal proof certificate identified upstream as g_wppconcrete6notwppfrompointndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcnselfbasendv (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.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))

Checked nominal proof certificate identified upstream as g_hwcnselfbasendv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnpw13quoshiftf1ondv (A : SemanticCore.Class) (hyp_hnpw13quoshiftf1ondv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw1 A))) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnsiquomap A))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)))) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A)))))

Checked nominal proof certificate identified upstream as g_hnpw13quoshiftf1ondv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqcommonprecoverinjndv (D S E J : SemanticCore.Class) (hyp_hnqcommonprecoverinjndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hnqcommonprecoverinjndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem E Compiler.CompactSourceSyntax.synCvv)) (hyp_hnqcommonprecoverinjndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 J S (Compiler.CompactSourceSyntax.synChnord D))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqinc D (Compiler.CompactSourceSyntax.synCun D E)) J) S) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqinc E (Compiler.CompactSourceSyntax.synCun D E)))).imp (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqinc E (Compiler.CompactSourceSyntax.synCun D E))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqinc D (Compiler.CompactSourceSyntax.synCun D E)) J)) S) S (Compiler.CompactSourceSyntax.synChnord E)))

Checked nominal proof certificate identified upstream as g_hnqcommonprecoverinjndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part087.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcwehwcardsndv (D R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCnc D) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_ncwehwcardsndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomaprepvalcl3ndv (A C Q : SemanticCore.Class) (hyp_hnsiquomaprepvalcl3ndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem Q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni Q) (Compiler.CompactSourceSyntax.synCec C (Compiler.CompactSourceSyntax.synChwniso A))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsiquomap A) Q) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) (Compiler.CompactSourceSyntax.synCsn C)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 A)))))

Checked nominal proof certificate identified upstream as g_hnsiquomaprepvalcl3ndv.

Equations

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