first | done | rfl | intro h; simp [h]
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σPE.vars
val : Interface.Scheme.type σPE var
⊢ ¬var' = var → (if h : var' = var then some ((_ : var = var') ▸ val) else none) = none
no goals