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