have e := Equivalent.trans (Equivalent.symm rf₁.equiv) rf₂.equiv
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
⊢ rtr₁ = rtr₂
α : Type
inst✝ : Proper α
rtr₁ : α
as : ID ⇀ Value
rtr₂ rtr : α
rf₁ : Refresh rtr rtr₁ as
rf₂ : Refresh rtr rtr₂ as
e : rtr₁ ≈ rtr₂
⊢ rtr₁ = rtr₂