This file extends the
suffices tactics to allow the addition of hypotheses to
the context without requiring their proofs to be provided immediately.
Adds hypotheses to the context, turning them into goals to be proved later if their proof terms
aren't provided (
t: Option Term := none).
If the bound term is intended to be kept in the context, pass
keepTerm : Bool := true. This is
useful when extending the
let tactic, which is expected to show the proof term in the infoview.