Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk012ACompact002Part001.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1oeq3 (A B C F : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf1o F C A) (Compiler.CompactSourceSyntax.synWf1o F C B)))

Checked nominal proof certificate identified upstream as g_f1oeq3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_f1oeq23.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1of1 (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o F A B).imp (Compiler.CompactSourceSyntax.synWf1 F A B))

Checked nominal proof certificate identified upstream as g_f1of1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1of (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o F A B).imp (Compiler.CompactSourceSyntax.synWf F A B))

Checked nominal proof certificate identified upstream as g_f1of.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ofn (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o F A B).imp (Compiler.CompactSourceSyntax.synWfn F A))

Checked nominal proof certificate identified upstream as g_f1ofn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ofun (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o F A B).imp (Compiler.CompactSourceSyntax.synWfun F))

Checked nominal proof certificate identified upstream as g_f1ofun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1odm (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o F A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm F) A))

Checked nominal proof certificate identified upstream as g_f1odm.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDff1o2 (A B F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf1o F A B) (Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv F)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn F) B)))

Checked nominal proof certificate identified upstream as g_dff1o2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDff1o3 (A B F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf1o F A B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfo F A B) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv F))))

Checked nominal proof certificate identified upstream as g_dff1o3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ofo (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o F A B).imp (Compiler.CompactSourceSyntax.synWfo F A B))

Checked nominal proof certificate identified upstream as g_f1ofo.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDff1o4 (A B F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf1o F A B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCcnv F) B)))

Checked nominal proof certificate identified upstream as g_dff1o4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDff1o5 (A B F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf1o F A B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1 F A B) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn F) B)))

Checked nominal proof certificate identified upstream as g_dff1o5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1orn (A F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf1o F A (Compiler.CompactSourceSyntax.synCrn F)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv F))))

Checked nominal proof certificate identified upstream as g_f1orn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1f1orn (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 F A B).imp (Compiler.CompactSourceSyntax.synWf1o F A (Compiler.CompactSourceSyntax.synCrn F)))

Checked nominal proof certificate identified upstream as g_f1f1orn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ocnvb (A B F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf1o F A B) (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCcnv F) B A))

Checked nominal proof certificate identified upstream as g_f1ocnvb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ocnv (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o F A B).imp (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCcnv F) B A))

Checked nominal proof certificate identified upstream as g_f1ocnv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ores (A B C F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1 F A B) (Compiler.CompactSourceSyntax.synWss C A)).imp (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCres F C) C (Compiler.CompactSourceSyntax.synCima F C)))

Checked nominal proof certificate identified upstream as g_f1ores.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1oun (A B C D F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o F A B) (Compiler.CompactSourceSyntax.synWf1o G C D)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A C) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin B D) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCun F G) (Compiler.CompactSourceSyntax.synCun A C) (Compiler.CompactSourceSyntax.synCun B D)))

Checked nominal proof certificate identified upstream as g_f1oun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1oco (A B C F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o F B C) (Compiler.CompactSourceSyntax.synWf1o G A B)).imp (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCcom F G) A C))

Checked nominal proof certificate identified upstream as g_f1oco.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ococnv2 (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o F A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom F (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid B)))

Checked nominal proof certificate identified upstream as g_f1ococnv2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ococnv1 (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o F A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv F) F) (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid A)))

Checked nominal proof certificate identified upstream as g_f1ococnv1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1cnv (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1 F A B).imp (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCcnv F) (Compiler.CompactSourceSyntax.synCrn F) A))

Checked nominal proof certificate identified upstream as g_f1cnv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF10 (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0 A)

Checked nominal proof certificate identified upstream as g_f10.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1o00 (A F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf1o F Compiler.CompactSourceSyntax.synC0 A) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq F Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0)))

Checked nominal proof certificate identified upstream as g_f1o00.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1o0 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_f1o0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1oi (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid A) A A)

Checked nominal proof certificate identified upstream as g_f1oi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1ovi : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o Compiler.CompactSourceSyntax.synCid Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_f1ovi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1osn (A B : SemanticCore.Class) (hyp_f1osn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_f1osn_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A B)) (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCsn B))

Checked nominal proof certificate identified upstream as g_f1osn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1osng (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A B)) (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCsn B)))

Checked nominal proof certificate identified upstream as g_f1osng.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFv2 (x y : SemanticCore.Var) (A 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 (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cab x (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A F (SemanticCore.Class.cv y)) (SemanticCore.Wff.objEq y x))))))

Checked nominal proof certificate identified upstream as g_fv2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvprc (A F : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).neg.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_fvprc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfv (x y : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ 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 (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCfv F B)) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A (SemanticCore.Class.cv x)) (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr B F (SemanticCore.Class.cv y)) (SemanticCore.Wff.objEq y x))))))

Checked nominal proof certificate identified upstream as g_elfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFveq1 (A F G : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq F G).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCfv G A)))

Checked nominal proof certificate identified upstream as g_fveq1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFveq2 (A B F : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCfv F B)))

Checked nominal proof certificate identified upstream as g_fveq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFveq1i (A F G : SemanticCore.Class) (hyp_fveq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq F G)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCfv G A))

Checked nominal proof certificate identified upstream as g_fveq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gFveq1i A F G hyp_fveq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_fveq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gFveq1 A F G)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFveq1d (ph : SemanticCore.Wff) (A F G : SemanticCore.Class) (hyp_fveq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq F G))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCfv G A)))

Checked nominal proof certificate identified upstream as g_fveq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFveq2i (A B F : SemanticCore.Class) (hyp_fveq2i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCfv F B))

Checked nominal proof certificate identified upstream as g_fveq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gFveq2i A B F hyp_fveq2i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_fveq2i_1 (NFChoice.DirectNominalPrf.WPPReplay.gFveq2 A B F)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFveq2d (ph : SemanticCore.Wff) (A B F : SemanticCore.Class) (hyp_fveq2d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCfv F B)))

Checked nominal proof certificate identified upstream as g_fveq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvex (A F : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fvex.

Equations

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

Certificates from NominalWPPReplayChunk012ACompact002Part002.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFv3 (x y : SemanticCore.Var) (A 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 (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr A F (SemanticCore.Class.cv y)))) (Compiler.CompactSourceSyntax.synWeu y (Compiler.CompactSourceSyntax.synWbr A F (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_fv3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fvres.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunssfv (A F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWfun F) (Compiler.CompactSourceSyntax.synWss G F) (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm G))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCfv G A)))

Checked nominal proof certificate identified upstream as g_funssfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.g_tz6_12_1 (y : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_F_y : y ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A F B) (Compiler.CompactSourceSyntax.synWeu y (Compiler.CompactSourceSyntax.synWbr A F (SemanticCore.Class.cv y)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) B))

Checked nominal proof certificate identified upstream as g_tz6_12_1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.g_tz6_12_2 (y : SemanticCore.Var) (A F : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_F_y : y ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWeu y (Compiler.CompactSourceSyntax.synWbr A F (SemanticCore.Class.cv y))).neg.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_tz6_12_2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTz612c (y : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_F_y : y ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWeu y (Compiler.CompactSourceSyntax.synWbr A F (SemanticCore.Class.cv y))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) B) (Compiler.CompactSourceSyntax.synWbr A F B)))

Checked nominal proof certificate identified upstream as g_tz6_12c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNdmfv (A F : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm F)).neg.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_ndmfv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_elfvdm.

Equations

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

Certificates from NominalWPPReplayChunk012ACompact002Part003.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunbrfv (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun F).imp ((Compiler.CompactSourceSyntax.synWbr A F B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) B)))

Checked nominal proof certificate identified upstream as g_funbrfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunopfv (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun F).imp ((SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) F).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) B)))

Checked nominal proof certificate identified upstream as g_funopfv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fnbrfvb.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fnopfvb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunbrfvb (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.classEq (Compiler.CompactSourceSyntax.synCfv F A) B) (Compiler.CompactSourceSyntax.synWbr A F B)))

Checked nominal proof certificate identified upstream as g_funbrfvb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunopfvb (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.classEq (Compiler.CompactSourceSyntax.synCfv F A) B) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) F)))

Checked nominal proof certificate identified upstream as g_funopfvb.

Equations

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

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

Checked nominal proof certificate identified upstream as g_funbrfv2b.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnrnfv (x y : SemanticCore.Var) (A 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.synWfn F A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn F) (SemanticCore.Class.cab y (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_fnrnfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvelrnb (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.synWfn F A).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCrn F)) (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) B))))

Checked nominal proof certificate identified upstream as g_fvelrnb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfimafn (x y : SemanticCore.Var) (A 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.synWa (Compiler.CompactSourceSyntax.synWfun F) (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCdm F))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima F A) (SemanticCore.Class.cab y (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_dfimafn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunimass4 (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.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.synWral x A (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) B))))

Checked nominal proof certificate identified upstream as g_funimass4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvelima (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.synWfun F) (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCima F B))).imp (Compiler.CompactSourceSyntax.synWrex x B (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) A)))

Checked nominal proof certificate identified upstream as g_fvelima.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvelimab (x : SemanticCore.Var) (A B C F : SemanticCore.Class) (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.synWfn F A) (Compiler.CompactSourceSyntax.synWss B A)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCima F B)) (Compiler.CompactSourceSyntax.synWrex x B (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) C))))

Checked nominal proof certificate identified upstream as g_fvelimab.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fnsnfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunfv (A F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun F).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCima F (Compiler.CompactSourceSyntax.synCsn A)))))

Checked nominal proof certificate identified upstream as g_funfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvun (A F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun F) (Compiler.CompactSourceSyntax.synWfun G)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCdm F) (Compiler.CompactSourceSyntax.synCdm G)) Compiler.CompactSourceSyntax.synC0)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCun F G) A) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCfv G A))))

Checked nominal proof certificate identified upstream as g_fvun.

Equations

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

Certificates from NominalWPPReplayChunk012ACompact002Part004.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvun1 (A B F G X : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfn G B) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classMem X A))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCun F G) X) (Compiler.CompactSourceSyntax.synCfv F X)))

Checked nominal proof certificate identified upstream as g_fvun1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvun2 (A B F G X : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfn G B) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classMem X B))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCun F G) X) (Compiler.CompactSourceSyntax.synCfv G X)))

Checked nominal proof certificate identified upstream as g_fvun2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dmfco.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvco2 (A C F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn G A) (SemanticCore.Wff.classMem C A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcom F G) C) (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv G C))))

Checked nominal proof certificate identified upstream as g_fvco2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fvco.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fvco3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvopab3ig (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (A B C D 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_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_ch_x : x ∉ ch.fv) (dv_ch_y : y ∉ ch.fv) (dv_x_y : x ≠ y) (hyp_fvopab3ig_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_fvopab3ig_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_fvopab3ig_3 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C).imp (Compiler.CompactSourceSyntax.synWmo y ph))) (hyp_fvopab3ig_4 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C) ph)))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B D)).imp (ch.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) B)))

Checked nominal proof certificate identified upstream as g_fvopab3ig.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvopab4g (x y : SemanticCore.Var) (A B C D R F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_x_y : x ≠ y) (hyp_fvopab4g_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classEq B C))) (hyp_fvopab4g_2 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B))))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A D) (SemanticCore.Wff.classMem C R)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) C))

Checked nominal proof certificate identified upstream as g_fvopab4g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvopab4 (x y : SemanticCore.Var) (A B C D F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_x_y : x ≠ y) (hyp_fvopab4g_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classEq B C))) (hyp_fvopab4g_2 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B))))) (hyp_fvopab4_3 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem A D).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F A) C))

Checked nominal proof certificate identified upstream as g_fvopab4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqfnfv (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) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfn G A)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq F G) (Compiler.CompactSourceSyntax.synWral x A (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCfv G (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_eqfnfv.

Equations

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