simp [merge, Option.orElse]
case h
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
⊢ merge i i var = i var
case h
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
⊢ (match i var, fun x => i var with
    | some a, x => some a
    | none, b => b ()) =
    i var