kdrag.kernel.proj

kdrag.kernel.proj(p: Proof, n: int) → Proof

Project out of an And proof

>>> x = smt.Int("x")
>>> p = prove(smt.And(x > x - 1, x > x - 2, x > x - 3))
>>> proj(p, 0)
|- x > x - 1
>>> proj(p, 2)
|- x > x - 3

Parameters:

• p (Proof)

• n (int)

Return type:

Proof