Theorem: Interface?.merge_val₂ (Runtime/Interface.lean)

State before:
σ : Interface.Scheme
var : σ.vars
v : Interface.Scheme.type σ var
i₁ i₂ : Interface? σ
⊢ i₂ var = some v → merge i₁ i₂ var = some v
Tactic:
simp_all [merge, Option.orElse]
State after:
no goals