simp [h]
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
h : ¬var' = var
⊢ (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'
no goals