Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk011Compact001Part010.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfxp2 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCxp A B) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) A) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) B)))

Checked nominal proof certificate identified upstream as g_dfxp2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpexg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCxp A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_xpexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gXpex (A B : SemanticCore.Class) (hyp_xpex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_xpex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCxp A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_xpex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gResexg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCres A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_resexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gResex (A B : SemanticCore.Class) (hyp_resex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_resex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCres A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_resex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDffun2 (x y z : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun A) (SemanticCore.Wff.all x (SemanticCore.Wff.all y (SemanticCore.Wff.all z ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) A (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) A (SemanticCore.Class.cv z))).imp (SemanticCore.Wff.objEq y z))))))

Checked nominal proof certificate identified upstream as g_dffun2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDffun3 (x y z : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun A) (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWex z (SemanticCore.Wff.all y ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) A (SemanticCore.Class.cv y)).imp (SemanticCore.Wff.objEq y z))))))

Checked nominal proof certificate identified upstream as g_dffun3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDffun4 (x y z : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_A_z : z ∉ A.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun A) (SemanticCore.Wff.all x (SemanticCore.Wff.all y (SemanticCore.Wff.all z ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv z)) A)).imp (SemanticCore.Wff.objEq y z))))))

Checked nominal proof certificate identified upstream as g_dffun4.

Equations

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

Certificates from NominalWPPReplayChunk011Compact001Part011.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDffun6f (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_x_y : x ≠ y) (hyp_dffun6f_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) (hyp_dffun6f_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc y A)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun A) (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWmo y (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) A (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_dffun6f.

Equations

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

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

Checked nominal proof certificate identified upstream as g_dffun6.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunmo (y : SemanticCore.Var) (A F : SemanticCore.Class) (dv_A_y : y ∉ A.fv) (dv_F_y : y ∉ F.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun F).imp (Compiler.CompactSourceSyntax.synWmo y (Compiler.CompactSourceSyntax.synWbr A F (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as g_funmo.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunss (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A B).imp ((Compiler.CompactSourceSyntax.synWfun B).imp (Compiler.CompactSourceSyntax.synWfun A)))

Checked nominal proof certificate identified upstream as g_funss.

Equations

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

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

Checked nominal proof certificate identified upstream as g_funeq.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFuneqi (A B : SemanticCore.Class) (hyp_funeqi_1 : Nominal.NPrf (SemanticCore.Wff.classEq A B)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun A) (Compiler.CompactSourceSyntax.synWfun B))

Checked nominal proof certificate identified upstream as g_funeqi.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gFuneqi A B hyp_funeqi_1 = NFChoice.DirectNominalPrf.Nominal.mp hyp_funeqi_1 (NFChoice.DirectNominalPrf.WPPReplay.gFuneq A B)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFuneqd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_funeqd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun A) (Compiler.CompactSourceSyntax.synWfun B)))

Checked nominal proof certificate identified upstream as g_funeqd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFuneu (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.synWfun F) (Compiler.CompactSourceSyntax.synWbr A F B)).imp (Compiler.CompactSourceSyntax.synWeu y (Compiler.CompactSourceSyntax.synWbr A F (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as g_funeu.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFuneu2 (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.synWfun F) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) F)).imp (Compiler.CompactSourceSyntax.synWeu y (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A (SemanticCore.Class.cv y)) F)))

Checked nominal proof certificate identified upstream as g_funeu2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunfn (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun A) (Compiler.CompactSourceSyntax.synWfn A (Compiler.CompactSourceSyntax.synCdm A)))

Checked nominal proof certificate identified upstream as g_funfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFuni : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfun Compiler.CompactSourceSyntax.synCid)

Checked nominal proof certificate identified upstream as g_funi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunopab (ph : SemanticCore.Wff) (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCopab x y ph)) (SemanticCore.Wff.all x (Compiler.CompactSourceSyntax.synWmo y ph)))

Checked nominal proof certificate identified upstream as g_funopab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunco (F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun F) (Compiler.CompactSourceSyntax.synWfun G)).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcom F G)))

Checked nominal proof certificate identified upstream as g_funco.

Equations

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

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

Checked nominal proof certificate identified upstream as g_funres.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunssres (F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun F) (Compiler.CompactSourceSyntax.synWss G F)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCres F (Compiler.CompactSourceSyntax.synCdm G)) G))

Checked nominal proof certificate identified upstream as g_funssres.

Equations

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

Certificates from NominalWPPReplayChunk011Compact001Part012.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunun (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 (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCun F G)))

Checked nominal proof certificate identified upstream as g_funun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunsn (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A B)))

Checked nominal proof certificate identified upstream as g_funsn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFnsn (A B : SemanticCore.Class) (_hyp_fnsn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fnsn_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop A B)) (Compiler.CompactSourceSyntax.synCsn A))

Checked nominal proof certificate identified upstream as g_fnsn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFun0 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfun Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_fun0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFuncnv2 (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv A)) (SemanticCore.Wff.all y (Compiler.CompactSourceSyntax.synWmo x (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) A (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_funcnv2.

Equations

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

Certificates from NominalWPPReplayChunk011Compact001Part013.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFununi (A : SemanticCore.Class) (f g : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_A_g : g ∉ A.fv) (dv_f_g : f ≠ g) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral f A (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synWral g A (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv f) (SemanticCore.Class.cv g)) (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv g) (SemanticCore.Class.cv f)))))).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCuni A)))

Checked nominal proof certificate identified upstream as g_fununi.

Equations

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

Certificates from NominalWPPReplayChunk011Compact001Part014.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFuncnvuni (A : SemanticCore.Class) (f g : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_A_g : g ∉ A.fv) (dv_f_g : f ≠ g) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral f A (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synWral g A (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv f) (SemanticCore.Class.cv g)) (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv g) (SemanticCore.Class.cv f)))))).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCuni A))))

Checked nominal proof certificate identified upstream as g_funcnvuni.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFun11uni (A : SemanticCore.Class) (f g : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_A_g : g ∉ A.fv) (dv_f_g : f ≠ g) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWral f A (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (Compiler.CompactSourceSyntax.synWral g A (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv f) (SemanticCore.Class.cv g)) (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv g) (SemanticCore.Class.cv f)))))).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCuni A)) (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCuni A)))))

Checked nominal proof certificate identified upstream as g_fun11uni.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFunres11 (A F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv F)).imp (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres F A))))

Checked nominal proof certificate identified upstream as g_funres11.

Equations

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

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

Checked nominal proof certificate identified upstream as g_funcnvres.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCnvresid (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid A)) (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid A))

Checked nominal proof certificate identified upstream as g_cnvresid.

Equations

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

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

Checked nominal proof certificate identified upstream as g_funcnvres2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_funimacnv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_funimass2.

Equations

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