Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk014Compact001Part051.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutclassordcl (B D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutclassordcl_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((SemanticCore.Wff.classMem B D).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D B) (Compiler.CompactSourceSyntax.synChwniso D)) (Compiler.CompactSourceSyntax.synChnord D)))

Checked nominal proof certificate identified upstream as g_hnwcutclassordcl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutmapf (D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutmapf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synChnwcutmap R D) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (Compiler.CompactSourceSyntax.synChnord D))

Checked nominal proof certificate identified upstream as g_hnwcutmapf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutmapval (D R : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutmapval_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnwcutmap R D) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))) (Compiler.CompactSourceSyntax.synChwniso D))))

Checked nominal proof certificate identified upstream as g_hnwcutmapval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutcodeltnoiso (x y : SemanticCore.Var) (D R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChwniso D) (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv y))).neg)

Checked nominal proof certificate identified upstream as g_hnwcutcodeltnoiso.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisoclasseqbcl (A B C : SemanticCore.Class) (hyp_hwnisoclasseqbcl_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn A))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec B (Compiler.CompactSourceSyntax.synChwniso A)) (Compiler.CompactSourceSyntax.synCec C (Compiler.CompactSourceSyntax.synChwniso A))) (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwniso A) C)))

Checked nominal proof certificate identified upstream as g_hwnisoclasseqbcl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutcodecncl (B D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutcodecncl_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((SemanticCore.Wff.classMem B D).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnwcutcode R D B) (Compiler.CompactSourceSyntax.synChwcn D)))

Checked nominal proof certificate identified upstream as g_hnwcutcodecncl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutclassltne (x y : SemanticCore.Var) (D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutclassltne_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChwniso D)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synChwniso D))).neg)

Checked nominal proof certificate identified upstream as g_hnwcutclassltne.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part052.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutclassinj (x y : SemanticCore.Var) (D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutclassinj_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D)).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChwniso D)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synChwniso D))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as g_hnwcutclassinj.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutclassinjcl (B C D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutclassinjcl_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B D) (SemanticCore.Wff.classMem C D)).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D B) (Compiler.CompactSourceSyntax.synChwniso D)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D C) (Compiler.CompactSourceSyntax.synChwniso D))).imp (SemanticCore.Wff.classEq B C)))

Checked nominal proof certificate identified upstream as g_hnwcutclassinjcl.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part053.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutmapf1 (D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutmapf1_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synChnwcutmap R D) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (Compiler.CompactSourceSyntax.synChnord D))

Checked nominal proof certificate identified upstream as g_hnwcutmapf1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqmap1exg (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnqmap1 A) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_hnqmap1exg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqmap1fn (A : SemanticCore.Class) (hyp_hnqmap1fn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A)))

Checked nominal proof certificate identified upstream as g_hnqmap1fn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqmap1val (u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (hyp_hnqmap1val_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A))))

Checked nominal proof certificate identified upstream as g_hnqmap1val.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqmap1f (A : SemanticCore.Class) (hyp_hnqmap1f_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synChnord A))

Checked nominal proof certificate identified upstream as g_hnqmap1f.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqmap1rn (A : SemanticCore.Class) (hyp_hnqmap1rn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqmap1 A)) (Compiler.CompactSourceSyntax.synChnord A))

Checked nominal proof certificate identified upstream as g_hnqmap1rn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrlnker (R X Y : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr X (Compiler.CompactSourceSyntax.synClnker R) Y) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr X R Y) (Compiler.CompactSourceSyntax.synWbr Y R X)))

Checked nominal proof certificate identified upstream as g_brlnker.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnkerex (R : SemanticCore.Class) (hyp_lnkerex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synClnker R) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lnkerex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEllnquo (x : SemanticCore.Var) (A B R : SemanticCore.Class) (_dv_A_B : Disjoint A.fv B.fv) (_dv_A_R : Disjoint A.fv R.fv) (dv_A_x : x ∉ A.fv) (_dv_B_R : Disjoint B.fv R.fv) (dv_B_x : x ∉ B.fv) (dv_R_x : x ∉ R.fv) (hyp_ellnquo_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synClnquo R A)) (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synClnker R)))))

Checked nominal proof certificate identified upstream as g_ellnquo.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part054.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefinssvvk : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Compiler.CompactSourceSyntax.synClefin (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_lefinssvvk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLtfinssvvk : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Compiler.CompactSourceSyntax.synCltfin (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_ltfinssvvk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLtfinunidkssvvk : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCun Compiler.CompactSourceSyntax.synCltfin Compiler.CompactSourceSyntax.synCidk) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_ltfinunidkssvvk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEllefinunidk (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) (Compiler.CompactSourceSyntax.synCun Compiler.CompactSourceSyntax.synCltfin Compiler.CompactSourceSyntax.synCidk)) (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synCltfin) (SemanticCore.Wff.classEq A B))))

Checked nominal proof certificate identified upstream as g_ellefinunidk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefinlteq0 (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W) (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_lefinlteq0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefinlteqall (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synCltfin) (SemanticCore.Wff.classEq A B))))

Checked nominal proof certificate identified upstream as g_lefinlteqall.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefinunidk : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synClefin (Compiler.CompactSourceSyntax.synCun Compiler.CompactSourceSyntax.synCltfin Compiler.CompactSourceSyntax.synCidk))

Checked nominal proof certificate identified upstream as g_lefinunidk.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefinex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synClefin Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_lefinex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKqrelbrg (A B C V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B V) (SemanticCore.Wff.classMem C W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop B C) (Compiler.CompactSourceSyntax.synCkqrel A)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B C) A)))

Checked nominal proof certificate identified upstream as g_kqrelbrg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKqlefinbr (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) B) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synClefin)))

Checked nominal proof certificate identified upstream as g_kqlefinbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefintrnn (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCnnc)).imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B C) Compiler.CompactSourceSyntax.synClefin)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A C) Compiler.CompactSourceSyntax.synClefin)))

Checked nominal proof certificate identified upstream as g_lefintrnn.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part055.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefinantinn (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc)).imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B A) Compiler.CompactSourceSyntax.synClefin)).imp (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_lefinantinn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLefinconnexnn (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc)).imp (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk A B) Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B A) Compiler.CompactSourceSyntax.synClefin)))

Checked nominal proof certificate identified upstream as g_lefinconnexnn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFinleor : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) Compiler.CompactSourceSyntax.synCstrict Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_finleor.

Equations

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