Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part016.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWeincsegcutorwholendv (x y : SemanticCore.Var) (D R : SemanticCore.Class) (dv_D_y : y ∉ D.fv) (dv_R_y : y ∉ R.fv) (dv_x_y : x ≠ y) (hyp_weincsegcutorwholendv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D).imp (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) D) (Compiler.CompactSourceSyntax.synWrex y D (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))))))))

Checked nominal proof certificate identified upstream as g_weincsegcutorwholendv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElwecutisoclterminalndv (x u : SemanticCore.Var) (D R S E K : SemanticCore.Class) (dv_D_u : u ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_E_u : u ∉ E.fv) (dv_E_x : x ∉ E.fv) (dv_K_u : u ∉ K.fv) (dv_K_x : x ∉ K.fv) (dv_R_u : u ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_S_u : u ∉ S.fv) (dv_S_x : x ∉ S.fv) (dv_u_x : u ≠ x) : Nominal.NPrf ((SemanticCore.Wff.classMem K Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem K (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) (Compiler.CompactSourceSyntax.synWrex x D (Compiler.CompactSourceSyntax.synWrex u E (Compiler.CompactSourceSyntax.synWiso K (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) (Compiler.CompactSourceSyntax.synCin S (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))))))))

Checked nominal proof certificate identified upstream as g_elwecutisoclterminalndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part017.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisouniondmcutorwholendv (y : SemanticCore.Var) (D R S E : SemanticCore.Class) (dv_D_y : y ∉ D.fv) (dv_E_y : y ∉ E.fv) (dv_R_y : y ∉ R.fv) (dv_S_y : y ∉ S.fv) (hyp_wecutisouniondmcutorwholendv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisouniondmcutorwholendv_2 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) D) (Compiler.CompactSourceSyntax.synWrex y D (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))))

Checked nominal proof certificate identified upstream as g_wecutisouniondmcutorwholendv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisounionrncutorwholendv (u : SemanticCore.Var) (D R S E : SemanticCore.Class) (dv_D_u : u ∉ D.fv) (dv_E_u : u ∉ E.fv) (dv_R_u : u ∉ R.fv) (dv_S_u : u ∉ S.fv) (hyp_wecutisounionrncutorwholendv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) (hyp_wecutisounionrncutorwholendv_2 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) E) (Compiler.CompactSourceSyntax.synWrex u E (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))))))

Checked nominal proof certificate identified upstream as g_wecutisounionrncutorwholendv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogencodeparts (x : SemanticCore.Var) (D R : SemanticCore.Class) (hyp_wecutisogencodeparts_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))))

Checked nominal proof certificate identified upstream as g_wecutisogencodeparts.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part018.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogenrawcl (A B C : SemanticCore.Class) (f r : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_A_r : r ∉ A.fv) (_dv_B_f : f ∉ B.fv) (dv_B_r : r ∉ B.fv) (_dv_C_f : f ∉ C.fv) (dv_C_r : r ∉ C.fv) (dv_f_r : f ≠ r) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn A))) (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st C) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd C))).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))) B) (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))) C)))))

Checked nominal proof certificate identified upstream as g_wecutisogenrawcl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogencodeinran (x : SemanticCore.Var) (D R : SemanticCore.Class) (hyp_wecutisogencodeinran_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnwcutrel R D))))

Checked nominal proof certificate identified upstream as g_wecutisogencodeinran.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogenrangedecode (x : SemanticCore.Var) (B D R : SemanticCore.Class) (dv_B_x : x ∉ B.fv) (dv_D_x : x ∉ D.fv) (dv_R_x : x ∉ R.fv) (hyp_wecutisogenrangedecode_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnwcutrel R D))).imp (Compiler.CompactSourceSyntax.synWrex x D (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_wecutisogenrangedecode.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogencodeambient (x : SemanticCore.Var) (D R : SemanticCore.Class) (hyp_wecutisogencodeambient_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChwcn Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_wecutisogencodeambient.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogennormbij (f r : SemanticCore.Var) : Nominal.NPrf ((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))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv f) Compiler.CompactSourceSyntax.synChwbij))

Checked nominal proof certificate identified upstream as g_wecutisogennormbij.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part019.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogenrawmem (B C D R S : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (r : SemanticCore.Var) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnwcutrel R D))) (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnwcutrel S E)))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv 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))) B) (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))) C))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCwecutisogen R D S E)))

Checked nominal proof certificate identified upstream as g_wecutisogenrawmem.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogenrawout (D R S : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (r : SemanticCore.Var) (dv_D_r : r ∉ D.fv) (dv_E_r : r ∉ E.fv) (dv_R_r : r ∉ R.fv) (dv_S_r : r ∉ S.fv) (dv_f_r : f ≠ r) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCwecutisogen R D S E)).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.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnwcutrel R D))) (SemanticCore.Wff.classMem (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))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnwcutrel S E)))))))

Checked nominal proof certificate identified upstream as g_wecutisogenrawout.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part020.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisogenfixedrev (x y : SemanticCore.Var) (D R S : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (r : SemanticCore.Var) (_dv_D_f : f ∉ D.fv) (_dv_D_r : r ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (_dv_E_f : f ∉ E.fv) (_dv_E_r : r ∉ E.fv) (dv_E_x : x ∉ E.fv) (dv_E_y : y ∉ E.fv) (_dv_R_f : f ∉ R.fv) (_dv_R_r : r ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (_dv_S_f : f ∉ S.fv) (_dv_S_r : r ∉ S.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (_dv_f_r : f ≠ r) (dv_f_x : f ≠ x) (dv_f_y : f ≠ y) (_dv_r_x : r ≠ x) (_dv_r_y : r ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) E)) (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))) (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x))) (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))) (Compiler.CompactSourceSyntax.synChnwcutcode S E (SemanticCore.Class.cv y)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))

Checked nominal proof certificate identified upstream as g_wecutisogenfixedrev.

Equations

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