simp [go]
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
⊢ go rtr cpt vs (hd :: tail✝)[Component.val cpt][i] = some v
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
⊢ (match vs hd with
      | none => go rtr cpt vs tail✝
      | some v => go (update rtr cpt hd v) cpt vs tail✝)[Component.val cpt][i] =
    some v