kdrag.contracts.lemmas

kdrag.contracts.lemmas(e: ExprRef, into_binders=True) → list[Proof]

Instantiate all contract lemmas found in a pexression. This sweeps the expression and instantiates the contract lemma with the arguments to the function. Once it goes under binders, this becomes more difficult, so it returns the quantified form of the lemmas