case h
a b c d d' : List Γ'
x : K'
⊢ update (elim a b c d) stack d' x = elim a b c d' x
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' = elim a b c d'
funext x
no goals
case h
a b c d d' : List Γ'
x : K'
⊢ update (elim a b c d) stack d' x = elim a b c d' x
cases x <;> rfl