Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk012ACompact002Part005.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqfnfvd (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A F G : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_F_x : x ∉ F.fv) (dv_G_x : x ∉ G.fv) (dv_ph_x : x ∉ ph.fv) (hyp_eqfnfvd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWfn F A))) (hyp_eqfnfvd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWfn G A))) (hyp_eqfnfvd_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCfv G (SemanticCore.Class.cv x))))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq F G))

Checked nominal proof certificate identified upstream as g_eqfnfvd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunfvop (A F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun F) (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm F))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A (Compiler.CompactSourceSyntax.synCfv F A)) F))

Checked nominal proof certificate identified upstream as g_funfvop.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunfvbrb (A F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun F).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm F)) (Compiler.CompactSourceSyntax.synWbr A F (Compiler.CompactSourceSyntax.synCfv F A))))

Checked nominal proof certificate identified upstream as g_funfvbrb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvimacnvi (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun F) (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv F) B))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F A) B))

Checked nominal proof certificate identified upstream as g_fvimacnvi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvimacnv (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun F) (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm F))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F A) B) (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv F) B))))

Checked nominal proof certificate identified upstream as g_fvimacnv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunimass3 (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun F) (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCdm F))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCima F A) B) (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv F) B))))

Checked nominal proof certificate identified upstream as g_funimass3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpreima (A B C F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfn F A).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv F) C)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B A) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F B) C))))

Checked nominal proof certificate identified upstream as g_elpreima.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFimacnv (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf F A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv F) B) A))

Checked nominal proof certificate identified upstream as g_fimacnv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvelrn (A F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun F) (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm F))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCrn F)))

Checked nominal proof certificate identified upstream as g_fvelrn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnfvelrn (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (SemanticCore.Wff.classMem B A)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F B) (Compiler.CompactSourceSyntax.synCrn F)))

Checked nominal proof certificate identified upstream as g_fnfvelrn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFfvelrn (A B C F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf F A B) (SemanticCore.Wff.classMem C A)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F C) B))

Checked nominal proof certificate identified upstream as g_ffvelrn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFfvelrni (A B C F : SemanticCore.Class) (hyp_ffvrni_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf F A B)) : Nominal.NPrf ((SemanticCore.Wff.classMem C A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F C) B))

Checked nominal proof certificate identified upstream as g_ffvelrni.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDffo3 (x y : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_F_x : x ∉ F.fv) (dv_F_y : y ∉ F.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfo F A B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf F A B) (Compiler.CompactSourceSyntax.synWral y B (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)))))))

Checked nominal proof certificate identified upstream as g_dffo3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFoelrn (x : SemanticCore.Var) (A B C F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_F_x : x ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfo F A B) (SemanticCore.Wff.classMem C B)).imp (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_foelrn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFfnfv (x : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_F_x : x ∉ F.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf F A B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWral x A (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) B))))

Checked nominal proof certificate identified upstream as g_ffnfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnfvrnss (x : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_F_x : x ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWral x A (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) B))).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) B))

Checked nominal proof certificate identified upstream as g_fnfvrnss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFsn (A B F : SemanticCore.Class) (hyp_fsn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fsn_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf F (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCsn B)) (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A B))))

Checked nominal proof certificate identified upstream as g_fsn.

Equations

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

Certificates from NominalWPPReplayChunk012ACompact002Part006.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFsn2 (A B F : SemanticCore.Class) (hyp_fsn2_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf F (Compiler.CompactSourceSyntax.synCsn A) B) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F A) B) (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A (Compiler.CompactSourceSyntax.synCfv F A))))))

Checked nominal proof certificate identified upstream as g_fsn2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRessnop0 (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A C).neg.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A B)) C) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_ressnop0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvconst (A B C F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf F A (Compiler.CompactSourceSyntax.synCsn B)) (SemanticCore.Wff.classMem C A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F C) B))

Checked nominal proof certificate identified upstream as g_fvconst.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvi (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCid A) A))

Checked nominal proof certificate identified upstream as g_fvi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvresi (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid A) B) B))

Checked nominal proof certificate identified upstream as g_fvresi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvunsn (A B C D : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWne B D).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop B C))) D) (Compiler.CompactSourceSyntax.synCfv A D)))

Checked nominal proof certificate identified upstream as g_fvunsn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvconst2g (A B C D : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B D) (SemanticCore.Wff.classMem C A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCxp A (Compiler.CompactSourceSyntax.synCsn B)) C) B))

Checked nominal proof certificate identified upstream as g_fvconst2g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvconst2 (A B C : SemanticCore.Class) (hyp_fvconst2_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem C A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCxp A (Compiler.CompactSourceSyntax.synCsn B)) C) B))

Checked nominal proof certificate identified upstream as g_fvconst2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunfvima (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun F) (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCdm F))).imp ((SemanticCore.Wff.classMem B A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F B) (Compiler.CompactSourceSyntax.synCima F A))))

Checked nominal proof certificate identified upstream as g_funfvima.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFniunfv (x : SemanticCore.Var) (A F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_F_x : x ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfn F A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCiun x A (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCrn F))))

Checked nominal proof certificate identified upstream as g_fniunfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFuniunfv (x : SemanticCore.Var) (A F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_F_x : x ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun F).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCiun x A (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCima F A))))

Checked nominal proof certificate identified upstream as g_funiunfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEluniima (x : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_F_x : x ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun F).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCima F A))) (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_eluniima.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElunirn (x : SemanticCore.Var) (A F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_F_x : x ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun F).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCrn F))) (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCdm F) (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_elunirn.

Equations

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

Certificates from NominalWPPReplayChunk012ACompact002Part007.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDff13 (x y : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_F_x : x ∉ F.fv) (dv_F_y : y ∉ F.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf1 F A B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf F A B) (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y A ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.objEq x y))))))

Checked nominal proof certificate identified upstream as g_dff13.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1fveq (A B C D F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1 F A B) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C A) (SemanticCore.Wff.classMem D A))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F C) (Compiler.CompactSourceSyntax.synCfv F D)) (SemanticCore.Wff.classEq C D)))

Checked nominal proof certificate identified upstream as g_f1fveq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1elima (A B F X Y : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWf1 F A B) (SemanticCore.Wff.classMem X A) (Compiler.CompactSourceSyntax.synWss Y A)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F X) (Compiler.CompactSourceSyntax.synCima F Y)) (SemanticCore.Wff.classMem X Y)))

Checked nominal proof certificate identified upstream as g_f1elima.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDff1o6 (x y : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_F_x : x ∉ F.fv) (dv_F_y : y ∉ F.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf1o F A B) (Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWfn F A) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn F) B) (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWral y A ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))))))

Checked nominal proof certificate identified upstream as g_dff1o6.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ocnvfv1 (A B C F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o F A B) (SemanticCore.Wff.classMem C A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv F) (Compiler.CompactSourceSyntax.synCfv F C)) C))

Checked nominal proof certificate identified upstream as g_f1ocnvfv1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ocnvfv2 (A B C F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o F A B) (SemanticCore.Wff.classMem C B)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv F) C)) C))

Checked nominal proof certificate identified upstream as g_f1ocnvfv2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ocnvfv (A B C D F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o F A B) (SemanticCore.Wff.classMem C A)).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F C) D).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv F) D) C)))

Checked nominal proof certificate identified upstream as g_f1ocnvfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ocnvfvb (A B C D F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWf1o F A B) (SemanticCore.Wff.classMem C A) (SemanticCore.Wff.classMem D B)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F C) D) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv F) D) C)))

Checked nominal proof certificate identified upstream as g_f1ocnvfvb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ocnvdm (A B C F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o F A B) (SemanticCore.Wff.classMem C B)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcnv F) C) A))

Checked nominal proof certificate identified upstream as g_f1ocnvdm.

Equations

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