kdrag.datatype.accessor_lemmas

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

Accessor lemmas for a datatype.

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