Theorem: Interface?.isPresent_def (Runtime/Interface.lean)

State before:
σ : Interface.Scheme
var : σ.vars
i : Interface? σ
⊢ isPresent i var = true ↔ ∃ v, i var = some v
Tactic:
simp [isPresent, Option.isSome_iff_exists]
State after:
no goals