intro cpt _ _ _ ho₁ ho₂
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
⊢ ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
cpt : Component.Valued
i✝ : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₁[Component.val cpt][i✝] = some o₁✝
ho₂ : rtr₂[Component.val cpt][i✝] = some o₂✝
⊢ o₁✝ = o₂✝