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