case act => injection (rf₁.acts     ▸ ho₁) ▸ rf₂.acts     ▸ ho₂
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
i✝ : Component.idType (Component.val Component.Valued.act)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.act)
ho₁ : rtr₁[Component.val Component.Valued.act][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.act][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
no goals