Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk011Compact001Part015.

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

Checked nominal proof certificate identified upstream as g_imadif.

Equations

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

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

Checked nominal proof certificate identified upstream as g_imain.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fneq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fneq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFneq1d (ph : SemanticCore.Wff) (A F G : SemanticCore.Class) (hyp_fneq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq F G))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfn G A)))

Checked nominal proof certificate identified upstream as g_fneq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFneq2d (ph : SemanticCore.Wff) (A B F : SemanticCore.Class) (hyp_fneq2d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfn F B)))

Checked nominal proof certificate identified upstream as g_fneq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFneq1i (A F G : SemanticCore.Class) (hyp_fneq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq F G)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfn G A))

Checked nominal proof certificate identified upstream as g_fneq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gFneq1i A F G hyp_fneq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_fneq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gFneq1 A F G)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFneq2i (A B F : SemanticCore.Class) (hyp_fneq2i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfn F B))

Checked nominal proof certificate identified upstream as g_fneq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gFneq2i A B F hyp_fneq2i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_fneq2i_1 (NFChoice.DirectNominalPrf.WPPReplay.gFneq2 A B F)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnfun (A F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfn F A).imp (Compiler.CompactSourceSyntax.synWfun F))

Checked nominal proof certificate identified upstream as g_fnfun.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fndm.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunfni (ph : SemanticCore.Wff) (A B F : SemanticCore.Class) (hyp_funfni_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun F) (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCdm F))).imp ph)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (SemanticCore.Wff.classMem B A)).imp ph)

Checked nominal proof certificate identified upstream as g_funfni.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fnbr.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fnop.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFneu (y : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_B_y : y ∉ B.fv) (dv_F_y : y ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (SemanticCore.Wff.classMem B A)).imp (Compiler.CompactSourceSyntax.synWeu y (Compiler.CompactSourceSyntax.synWbr B F (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as g_fneu.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFneu2 (y : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_B_y : y ∉ B.fv) (dv_F_y : y ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (SemanticCore.Wff.classMem B A)).imp (Compiler.CompactSourceSyntax.synWeu y (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop B (SemanticCore.Class.cv y)) F)))

Checked nominal proof certificate identified upstream as g_fneu2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fnun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnco (A B F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfn G B) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) A)).imp (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCcom F G) B))

Checked nominal proof certificate identified upstream as g_fnco.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnresdm (A F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfn F A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres F A) F))

Checked nominal proof certificate identified upstream as g_fnresdm.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnssresb (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfn F A).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCres F B) B) (Compiler.CompactSourceSyntax.synWss B A)))

Checked nominal proof certificate identified upstream as g_fnssresb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnssres (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWss B A)).imp (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCres F B) B))

Checked nominal proof certificate identified upstream as g_fnssres.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fnresin1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnres (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.synWb (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCres F A) A) (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWeu y (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) F (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_fnres.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fnresi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFn0 (F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfn F Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq F Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_fn0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnopabg (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) (hyp_fnopabg_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph)))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (Compiler.CompactSourceSyntax.synWeu y ph)) (Compiler.CompactSourceSyntax.synWfn F A))

Checked nominal proof certificate identified upstream as g_fnopabg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnopab2g (x y : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) (hyp_fnopab2g_1 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral x A (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWfn F A))

Checked nominal proof certificate identified upstream as g_fnopab2g.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnopab (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (A F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) (hyp_fnopab_1 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWeu y ph))) (hyp_fnopab_2 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph)))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn F A)

Checked nominal proof certificate identified upstream as g_fnopab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnopab2 (x y : SemanticCore.Var) (A B F : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_x_y : x ≠ y) (hyp_fnopab2_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_fnopab2_2 : Nominal.NPrf (SemanticCore.Wff.classEq F (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) B))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn F A)

Checked nominal proof certificate identified upstream as g_fnopab2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFeq1 (A B F G : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq F G).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf F A B) (Compiler.CompactSourceSyntax.synWf G A B)))

Checked nominal proof certificate identified upstream as g_feq1.

Equations

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

Certificates from NominalWPPReplayChunk011Compact001Part016.

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

Checked nominal proof certificate identified upstream as g_feq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_feq3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFeq1i (A B F G : SemanticCore.Class) (hyp_feq1i_1 : Nominal.NPrf (SemanticCore.Wff.classEq F G)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf F A B) (Compiler.CompactSourceSyntax.synWf G A B))

Checked nominal proof certificate identified upstream as g_feq1i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gFeq1i A B F G hyp_feq1i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_feq1i_1 (NFChoice.DirectNominalPrf.WPPReplay.gFeq1 A B F G)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFeq2i (A B C F : SemanticCore.Class) (hyp_feq2i_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf F A C) (Compiler.CompactSourceSyntax.synWf F B C))

Checked nominal proof certificate identified upstream as g_feq2i.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gFeq2i A B C F hyp_feq2i_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_feq2i_1 (NFChoice.DirectNominalPrf.WPPReplay.gFeq2 A B C F)

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

Checked nominal proof certificate identified upstream as g_ffn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDffn2 (A F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWf F A Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_dffn2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ffun.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fdm.

Equations

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

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

Checked nominal proof certificate identified upstream as g_frn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDffn3 (A F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWf F A (Compiler.CompactSourceSyntax.synCrn F)))

Checked nominal proof certificate identified upstream as g_dffn3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFss (A B C F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf F A B) (Compiler.CompactSourceSyntax.synWss B C)).imp (Compiler.CompactSourceSyntax.synWf F A C))

Checked nominal proof certificate identified upstream as g_fss.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fco.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fssxp.

Equations

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

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

Checked nominal proof certificate identified upstream as g_opelf.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnfco (A B F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWf G B A)).imp (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCcom F G) B))

Checked nominal proof certificate identified upstream as g_fnfco.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFssres (A B C F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf F A B) (Compiler.CompactSourceSyntax.synWss C A)).imp (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synCres F C) C B))

Checked nominal proof certificate identified upstream as g_fssres.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fcoi1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFeu (y : SemanticCore.Var) (A B C F : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_B_y : y ∉ B.fv) (dv_C_y : y ∉ C.fv) (dv_F_y : y ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf F A B) (SemanticCore.Wff.classMem C A)).imp (Compiler.CompactSourceSyntax.synWreu y B (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop C (SemanticCore.Class.cv y)) F)))

Checked nominal proof certificate identified upstream as g_feu.

Equations

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

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

Checked nominal proof certificate identified upstream as g_f0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFconst (A B : SemanticCore.Class) (hyp_fconst_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synCxp A (Compiler.CompactSourceSyntax.synCsn B)) A (Compiler.CompactSourceSyntax.synCsn B))

Checked nominal proof certificate identified upstream as g_fconst.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFconstg (A B V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B V).imp (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synCxp A (Compiler.CompactSourceSyntax.synCsn B)) A (Compiler.CompactSourceSyntax.synCsn B)))

Checked nominal proof certificate identified upstream as g_fconstg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnconstg (A B V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B V).imp (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCxp A (Compiler.CompactSourceSyntax.synCsn B)) A))

Checked nominal proof certificate identified upstream as g_fnconstg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1eq1 (A B F G : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq F G).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWf1 F A B) (Compiler.CompactSourceSyntax.synWf1 G A B)))

Checked nominal proof certificate identified upstream as g_f1eq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_f1eq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_f1eq3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDff12 (x y : SemanticCore.Var) (A B F : SemanticCore.Class) (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) (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWmo x (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) F (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_dff12.

Equations

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

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

Checked nominal proof certificate identified upstream as g_f1f.

Equations

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

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

Checked nominal proof certificate identified upstream as g_f1fn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_f1ss.

Equations

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

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

Checked nominal proof certificate identified upstream as g_f1co.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFoeq1 (A B F G : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq F G).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfo F A B) (Compiler.CompactSourceSyntax.synWfo G A B)))

Checked nominal proof certificate identified upstream as g_foeq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_foeq2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_foeq3.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fof.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fofun.

Equations

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

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

Checked nominal proof certificate identified upstream as g_fofn.

Equations

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

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

Checked nominal proof certificate identified upstream as g_forn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDffo2 (A B F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfo F A B) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf F A B) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn F) B)))

Checked nominal proof certificate identified upstream as g_dffo2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_foima.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDffn4 (A F : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfo F A (Compiler.CompactSourceSyntax.synCrn F)))

Checked nominal proof certificate identified upstream as g_dffn4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFores (A F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun F) (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCdm F))).imp (Compiler.CompactSourceSyntax.synWfo (Compiler.CompactSourceSyntax.synCres F A) A (Compiler.CompactSourceSyntax.synCima F A)))

Checked nominal proof certificate identified upstream as g_fores.

Equations

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

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

Checked nominal proof certificate identified upstream as g_foco.

Equations

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

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

Checked nominal proof certificate identified upstream as g_f1oeq1.

Equations

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

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

Checked nominal proof certificate identified upstream as g_f1oeq2.

Equations

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