cases cpt
α : 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₂✝
case inp
α : 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.inp)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.inp)
ho₁ : rtr₁[Component.val Component.Valued.inp][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.inp][i✝] = some o₂✝
⊢ o₁✝ = o₂✝

case out
α : 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.out)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.out)
ho₁ : rtr₁[Component.val Component.Valued.out][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.out][i✝] = some o₂✝
⊢ o₁✝ = o₂✝

case stv
α : 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.stv)
o₁✝ o₂✝ : Component.type α (Component.val Component.Valued.stv)
ho₁ : rtr₁[Component.val Component.Valued.stv][i✝] = some o₁✝
ho₂ : rtr₂[Component.val Component.Valued.stv][i✝] = some o₂✝
⊢ o₁✝ = o₂✝

case act
α : 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₂✝