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