induction ids generalizing rtr <;> simp [go]
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
ids : List ID
⊢ rtr ≈ go rtr cpt vs ids
case nil
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
rtr : α
⊢ rtr ≈ rtr

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