cases s <;> simp [extend]
α : Type
inst✝ : Reactor α
rtr : α
i : ID
cpt : Component
j : ID
o : Component.type (Component.type α Component.rtr) cpt
o' : Component.type α cpt
s : StrictMember Component.rtr i rtr
h : object s{cpt}{j} = some o
hf : rtr{cpt}{j} = some o'
⊢ extend s h ≠ final hf
no goals