kdrag.datatype.distinct_lemmas

kdrag.datatype.distinct_lemmas(dt: DatatypeSortRef) → list[Proof]

Constructors are distinct lemmas.

>>> import kdrag.theories.nat as nat
>>> distinct_lemmas(nat.Nat)[0]
|- ForAll(x!..., S(x!...) != Z)