Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk014Compact001Part023.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcodemap2ex (A B C R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_C_R : Disjoint C.fv R.fv) (hyp_fdcodemap2ex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodemap2ex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodemap2ex_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodemap2ex_4 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdcodemap2 R A B C) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_fdcodemap2ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcodeeqrnmap2 (A B C R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_C_R : Disjoint C.fv R.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdcode R A B C) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCfdcodemap2 R A B C)))

Checked nominal proof certificate identified upstream as g_fdcodeeqrnmap2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcodeex2 (A B C R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_C_R : Disjoint C.fv R.fv) (hyp_fdcodeex2_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodeex2_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodeex2_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodeex2_4 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdcode R A B C) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_fdcodeex2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcodeelpwpw2 (A B C R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_C_R : Disjoint C.fv R.fv) (hyp_fdcodeelpwpw2_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodeelpwpw2_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodeelpwpw2_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodeelpwpw2_4 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdcode R A B C) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCfdif R A B)))))

Checked nominal proof certificate identified upstream as g_fdcodeelpwpw2.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part024.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdroweq4 (A B C D R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_D : Disjoint A.fv D.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_D : Disjoint B.fv D.fv) (dv_B_R : Disjoint B.fv R.fv) (_dv_C_D : Disjoint C.fv D.fv) (dv_C_R : Disjoint C.fv R.fv) (dv_D_R : Disjoint D.fv R.fv) : Nominal.NPrf ((SemanticCore.Wff.classEq C D).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdrow R A B C) (Compiler.CompactSourceSyntax.synCfdrow R A B D)))

Checked nominal proof certificate identified upstream as g_fdroweq4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfdcode2g (x : SemanticCore.Var) (A B C D R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_A_x : x ∉ A.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_B_x : x ∉ B.fv) (dv_C_R : Disjoint C.fv R.fv) (dv_C_x : x ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_R_x : x ∉ R.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfdcode R A B C)) (Compiler.CompactSourceSyntax.synWrex x C (SemanticCore.Wff.classEq D (Compiler.CompactSourceSyntax.synCfdrow R A B (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_elfdcode2g.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part025.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcodesub2 (A B C D R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_D : Disjoint A.fv D.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_D : Disjoint B.fv D.fv) (dv_B_R : Disjoint B.fv R.fv) (_dv_C_D : Disjoint C.fv D.fv) (dv_C_R : Disjoint C.fv R.fv) (dv_D_R : Disjoint D.fv R.fv) (hyp_fdcodesub2_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodesub2_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodesub2_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCpw B))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C A) (SemanticCore.Wff.classMem D A))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdcode R A B C) (Compiler.CompactSourceSyntax.synCfdcode R A B D))).imp (Compiler.CompactSourceSyntax.synWss C D))

Checked nominal proof certificate identified upstream as g_fdcodesub2.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part026.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcodeinj2 (A B C D R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_D : Disjoint A.fv D.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_D : Disjoint B.fv D.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_C_D : Disjoint C.fv D.fv) (dv_C_R : Disjoint C.fv R.fv) (dv_D_R : Disjoint D.fv R.fv) (hyp_fdcodeinj2_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodeinj2_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcodeinj2_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCpw B))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C A) (SemanticCore.Wff.classMem D A))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdcode R A B C) (Compiler.CompactSourceSyntax.synCfdcode R A B D))).imp (SemanticCore.Wff.classEq C D))

Checked nominal proof certificate identified upstream as g_fdcodeinj2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppimagefn (R : SemanticCore.Class) (hyp_wppimagefn_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCimage R) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppimagefn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppfvimage (A R : SemanticCore.Class) (_dv_A_R : Disjoint A.fv R.fv) (hyp_wppfvimage_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_wppfvimage_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCimage R) A) (Compiler.CompactSourceSyntax.synCima R A))

Checked nominal proof certificate identified upstream as g_wppfvimage.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdpointrelex (A : SemanticCore.Class) (hyp_fdpointrelex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdpointrel A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fdpointrelex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdglobalrowex (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdglobalrowex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdglobalrowex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdglobalrowex_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdglobalrowmap R A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fdglobalrowex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdglobalrowval (u : SemanticCore.Var) (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_A_u : u ∉ A.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_B_u : u ∉ B.fv) (dv_R_u : u ∉ R.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdglobalrowmap R A B) (Compiler.CompactSourceSyntax.synCmpt u (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni A))) (Compiler.CompactSourceSyntax.synCfdrowfib R A B (SemanticCore.Class.cv u)))))

Checked nominal proof certificate identified upstream as g_fdglobalrowval.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part027.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdpointimage (A : SemanticCore.Class) (c : SemanticCore.Var) (_dv_A_c : c ∉ A.fv) (_hyp_fdpointimage_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv c) A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCfdpointrel A) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv c)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv c)))))

Checked nominal proof certificate identified upstream as g_fdpointimage.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdglobalrowima (A B C R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_C_R : Disjoint C.fv R.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (SemanticCore.Wff.classMem C A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCfdglobalrowmap R A B) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 C))) (Compiler.CompactSourceSyntax.synCfdcode R A B C)))

Checked nominal proof certificate identified upstream as g_fdglobalrowima.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcolcodemapex (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdcolcodemapex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodemapex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodemapex_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdcolcodemap R A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_fdcolcodemapex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcolcodemapfn (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdcolcodemapfn_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodemapfn_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodemapfn_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCfdcolcodemap R A B) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))))

Checked nominal proof certificate identified upstream as g_fdcolcodemapfn.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part028.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcolcodemapval (A B R : SemanticCore.Class) (q : SemanticCore.Var) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_A_q : q ∉ A.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_B_q : q ∉ B.fv) (dv_R_q : q ∉ R.fv) (hyp_fdcolcodemapval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodemapval_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodemapval_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfdcolcodemap R A B) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCfdcode R A B (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))

Checked nominal proof certificate identified upstream as g_fdcolcodemapval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcolcodemapf (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdcolcodemapf_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodemapf_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdcolcodemapf_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synCfdcolcodemap R A B) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A)) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCfdif R A B)))))

Checked nominal proof certificate identified upstream as g_fdcolcodemapf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcolcodearg (A : SemanticCore.Class) (q : SemanticCore.Var) (_dv_A_q : q ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))))

Checked nominal proof certificate identified upstream as g_fdcolcodearg.

Equations

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