LeanPool.NFWeakPartition.NominalWPPReplayChunk008

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSnelpw1 (A B : SemanticCore.Class) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn A) (Compiler.CompactSourceSyntax.synCpw1 B)) (SemanticCore.Wff.classMem A B))

Checked nominal proof certificate identified upstream as g_snelpw1.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpw11c (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_elpw11c.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpw121c (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))))

Checked nominal proof certificate identified upstream as g_elpw121c.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpw131c (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))))

Checked nominal proof certificate identified upstream as g_elpw131c.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpw141c (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :

Checked nominal proof certificate identified upstream as g_elpw141c.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpw151c (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :

Checked nominal proof certificate identified upstream as g_elpw151c.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpw161c (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :

Checked nominal proof certificate identified upstream as g_elpw161c.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpw171c (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :

Checked nominal proof certificate identified upstream as g_elpw171c.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpw181c (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :

Checked nominal proof certificate identified upstream as g_elpw181c.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElpw191c (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :

Checked nominal proof certificate identified upstream as g_elpw191c.

Equations

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

Instances For