case none => exact hi
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi : ∀ {rtr : α}, rtr ≈ go rtr cpt vs tail✝
rtr : α
⊢ rtr ≈
    match none with
    | none => go rtr cpt vs tail✝
    | some v => go (update rtr cpt hd v) cpt vs tail✝
no goals