kdrag.tele.Fin

kdrag.tele.Fin(n)

>>> m = smt.Int("m")
>>> Fin(3)
Lambda(x, And(Lambda(n, n >= 0)[x], x < 3))
>>> kd.prove(smt.Not(smt.Exists([m], Fin(0)[m])))
|= Not(Exists(m,
        Lambda(x, And(Lambda(n, n >= 0)[x], x < 0))[m]))