Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part006.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSiecsnndv (u : SemanticCore.Var) (R : SemanticCore.Class) (_dv_R_u : u ∉ R.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCsi R)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) R)))

Checked nominal proof certificate identified upstream as g_siecsnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSiecsnclndv (C R : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCsn C) (Compiler.CompactSourceSyntax.synCsi R)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCec C R))))

Checked nominal proof certificate identified upstream as g_siecsnclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1oclassimfreeclndv (v : SemanticCore.Var) (A B Q S T F : SemanticCore.Class) (dv_A_v : v ∉ A.fv) (_dv_B_v : v ∉ B.fv) (dv_F_v : v ∉ F.fv) (dv_Q_v : v ∉ Q.fv) (dv_S_v : v ∉ S.fv) (dv_T_v : v ∉ T.fv) (hyp_f1oclassimfreeclndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o F A B)) (hyp_f1oclassimfreeclndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCec Q T) A)) (hyp_f1oclassimfreeclndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv F Q) S) B)) (hyp_f1oclassimfreeclndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral v A (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr Q T (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv F Q) S (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv v)))))) (_hyp_f1oclassimfreeclndv_5 : Nominal.NPrf (SemanticCore.Wff.classMem Q A)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima F (Compiler.CompactSourceSyntax.synCec Q T)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv F Q) S))

Checked nominal proof certificate identified upstream as g_f1oclassimfreeclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapkernelclndv (A Q : SemanticCore.Class) (r : SemanticCore.Var) (dv_A_r : r ∉ A.fv) (_dv_Q_r : r ∉ Q.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem Q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A))).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr Q (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso A)) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) Q) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 A)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) (SemanticCore.Class.cv r))))))

Checked nominal proof certificate identified upstream as g_hnsicodemapkernelclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapclassimclndv (A Q : SemanticCore.Class) (hyp_hnsicodemapclassimclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_hnsicodemapclassimclndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem Q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A)))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChnsicodemap A) (Compiler.CompactSourceSyntax.synCec Q (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso A)))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) Q) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 A))))

Checked nominal proof certificate identified upstream as g_hnsicodemapclassimclndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part007.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapclassimdndv (A : SemanticCore.Class) (q : SemanticCore.Var) (_dv_A_q : q ∉ A.fv) (hyp_hnsicodemapclassimdndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChnsicodemap A) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso A)))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 A)))))

Checked nominal proof certificate identified upstream as g_hnsicodemapclassimdndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapclassimcldndv (A Q : SemanticCore.Class) (hyp_hnsicodemapclassimcldndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem Q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChnsicodemap A) (Compiler.CompactSourceSyntax.synCec Q (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso A)))) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) Q) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 A)))))

Checked nominal proof certificate identified upstream as g_hnsicodemapclassimcldndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhnordclndv (u : SemanticCore.Var) (A X : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_X_u : u ∉ X.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem X (Compiler.CompactSourceSyntax.synChnord A)) (Compiler.CompactSourceSyntax.synWrex u (Compiler.CompactSourceSyntax.synChwcn A) (SemanticCore.Wff.classEq X (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A))))))

Checked nominal proof certificate identified upstream as g_elhnordclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomapfvhnordndv (A : SemanticCore.Class) (q : SemanticCore.Var) (dv_A_q : q ∉ A.fv) (hyp_hnsiquomapfvhnordndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsiquomap A) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 A))))

Checked nominal proof certificate identified upstream as g_hnsiquomapfvhnordndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomapvalclndv (A Q : SemanticCore.Class) (hyp_hnsiquomapvalclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem Q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsiquomap A) Q) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChnsicodemap A) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni Q)))))

Checked nominal proof certificate identified upstream as g_hnsiquomapvalclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomapfndv (A : SemanticCore.Class) (hyp_hnsiquomapfndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synChnsiquomap A) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 A)))

Checked nominal proof certificate identified upstream as g_hnsiquomapfndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part008.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomappreexndv (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (_dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) (hyp_hnsiquomappreexndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 A))).imp (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsiquomap A) (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_hnsiquomappreexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomapfondv (A : SemanticCore.Class) (hyp_hnsiquomapfondv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfo (Compiler.CompactSourceSyntax.synChnsiquomap A) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 A)))

Checked nominal proof certificate identified upstream as g_hnsiquomapfondv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapkernelcl2ndv (A P Q : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem Q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A))).imp ((SemanticCore.Wff.classMem P (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr Q (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso A)) P) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) Q) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 A)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) P)))))

Checked nominal proof certificate identified upstream as g_hnsicodemapkernelcl2ndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part009.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomaprepvalndv (u : SemanticCore.Var) (A : SemanticCore.Class) (q : SemanticCore.Var) (dv_A_q : q ∉ A.fv) (dv_A_u : u ∉ A.fv) (_dv_q_u : q ≠ u) (hyp_hnsiquomaprepvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsiquomap A) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 A)))))

Checked nominal proof certificate identified upstream as g_hnsiquomaprepvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnordpw1repndv (u : SemanticCore.Var) (A : SemanticCore.Class) (q : SemanticCore.Var) (_dv_A_q : q ∉ A.fv) (_dv_A_u : u ∉ A.fv) (_dv_q_u : q ≠ u) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A))))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A)))))

Checked nominal proof certificate identified upstream as g_hnordpw1repndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrsnsiandv (A B R : SemanticCore.Class) (_dv_A_R : Disjoint A.fv R.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCsi R) (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synWbr A R B)))

Checked nominal proof certificate identified upstream as g_brsnsiandv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part010.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomapfvineqndv (A : SemanticCore.Class) (s q : SemanticCore.Var) (dv_A_q : q ∉ A.fv) (dv_A_s : s ∉ A.fv) (_dv_q_s : q ≠ s) (hyp_hnsiquomapfvineqndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv s) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)))).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsiquomap A) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsiquomap A) (SemanticCore.Class.cv s))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv q) (SemanticCore.Class.cv s))))

Checked nominal proof certificate identified upstream as g_hnsiquomapfvineqndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part011.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomapf1ndv (A : SemanticCore.Class) (hyp_hnsiquomapf1ndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synChnsiquomap A) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 A)))

Checked nominal proof certificate identified upstream as g_hnsiquomapf1ndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomapf1ondv (A : SemanticCore.Class) (hyp_hnsiquomapf1ondv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synChnsiquomap A) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 A)))

Checked nominal proof certificate identified upstream as g_hnsiquomapf1ondv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnordpw1shiftenndv (A : SemanticCore.Class) (hyp_hnordpw1shiftenndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)) Compiler.CompactSourceSyntax.synCen (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 A)))

Checked nominal proof certificate identified upstream as g_hnordpw1shiftenndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardtcshiftndv (A : SemanticCore.Class) (hyp_hncardtcshiftndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard A)) (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCpw1 A)))

Checked nominal proof certificate identified upstream as g_hncardtcshiftndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppconcrete6fntc7hncard1valndv : Nominal.NPrf (SemanticCore.Wff.classEq (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.synChncard (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))))

Checked nominal proof certificate identified upstream as g_wppconcrete6fntc7hncard1valndv.

Equations

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