split
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
case h.h_1
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
x✝¹ : Option (Interface.Scheme.type σ✝ var)
x✝ : Unit → Option (Interface.Scheme.type σ✝ var)
a✝ : Interface.Scheme.type σ✝ var
heq✝ : i var = some a✝
⊢ some a✝ = i var

case h.h_2
σ✝ : Interface.Scheme
i : Interface? σ✝
var : σ✝.vars
x✝¹ : Option (Interface.Scheme.type σ✝ var)
x✝ : Unit → Option (Interface.Scheme.type σ✝ var)
heq✝ : i var = none
⊢ (fun x => i var) () = i var