Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk015Compact001Part037.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachincballfin (C F N : SemanticCore.Class) (dv_C_F : Disjoint C.fv F.fv) (hyp_wppreachincballfin_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachincballfin_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classMem N (Compiler.CompactSourceSyntax.synCwppreachincb F C)))

Checked nominal proof certificate identified upstream as g_wppreachincballfin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachpowlayers (C F N : SemanticCore.Class) (d : SemanticCore.Var) (dv_C_F : Disjoint C.fv F.fv) (dv_C_d : d ∉ C.fv) (dv_F_d : d ∉ F.fv) (dv_N_d : d ∉ N.fv) (hyp_wppreachpowlayers_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachpowlayers_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWral d (Compiler.CompactSourceSyntax.synCdm F) (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synCtc N))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C) (Compiler.CompactSourceSyntax.synCsn N))))))

Checked nominal proof certificate identified upstream as g_wppreachpowlayers.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowlayerorbcl (B C D F : SemanticCore.Class) (dv_C_F : Disjoint C.fv F.fv) (hyp_wpppowlayerorbcl_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wpppowlayerorbcl_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wpppowlayerorbcl_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C) (Compiler.CompactSourceSyntax.synCsn B))) (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) B))))

Checked nominal proof certificate identified upstream as g_wpppowlayerorbcl.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part038.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachlayerorbfin (C D F N : SemanticCore.Class) (dv_C_F : Disjoint C.fv F.fv) (hyp_wppreachlayerorbfin_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppreachlayerorbfin_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppreachlayerorbfin_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synCtc N))) (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) N))))

Checked nominal proof certificate identified upstream as g_wppreachlayerorbfin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gStrictsegdifinindv (x : SemanticCore.Var) (D R : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (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.synCdif (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv R) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))

Checked nominal proof certificate identified upstream as g_strictsegdifinindv.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part039.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisoendpointseqndv (x y : SemanticCore.Var) (D R H : SemanticCore.Class) (hyp_wecutisoendpointseqndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D)) (SemanticCore.Wff.classMem H Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWiso H (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 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 y)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))) (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 y)))))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))

Checked nominal proof certificate identified upstream as g_wecutisoendpointseqndv.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part040.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisoendpointseqclndv (B C D R H : SemanticCore.Class) (hyp_wecutisoendpointseqclndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B D) (SemanticCore.Wff.classMem C D)) (SemanticCore.Wff.classMem H Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWiso H (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 B))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn B))))) (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 C))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn C))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn B))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn C))))).imp (SemanticCore.Wff.classEq B C))

Checked nominal proof certificate identified upstream as g_wecutisoendpointseqclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gStrictsegdifiniclndv (B D R : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn B))) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv R) (Compiler.CompactSourceSyntax.synCsn B))) (Compiler.CompactSourceSyntax.synCsn B))))

Checked nominal proof certificate identified upstream as g_strictsegdifiniclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsostrictsegimandv (x : SemanticCore.Var) (D R S E H : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso H R S D E) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima H (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 (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv x)))))))

Checked nominal proof certificate identified upstream as g_isostrictsegimandv.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part041.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsostrictsegresndv (x : SemanticCore.Var) (D R S E H : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso H R S D E) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D)).imp (Compiler.CompactSourceSyntax.synWiso (Compiler.CompactSourceSyntax.synCres H (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 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 (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv x))))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv H (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 E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv x)))))))

Checked nominal proof certificate identified upstream as g_isostrictsegresndv.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part042.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWeisouniquecl (D R S E F G : SemanticCore.Class) (hyp_weisouniquecl_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_weisouniquecl_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso F R S D E) (Compiler.CompactSourceSyntax.synWiso G R S D E))).imp (SemanticCore.Wff.classEq F G))

Checked nominal proof certificate identified upstream as g_weisouniquecl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisouniquecl (B C D R S E F G : SemanticCore.Class) (hyp_wecutisouniquecl_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisouniquecl_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso F (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 B))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn B))))) (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 C))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn C))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn B))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn C)))) (Compiler.CompactSourceSyntax.synWiso G (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 B))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn B))))) (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 C))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn C))))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn B))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn C)))))).imp (SemanticCore.Wff.classEq F G))

Checked nominal proof certificate identified upstream as g_wecutisouniquecl.

Equations

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