exact final _ _
case nested.final
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝⁴ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
a✝³ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝² : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝¹ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝¹
o✝ : Component.type α c
a✝ : rtr₂✝{c}{j} = some o✝
⊢ StrictMember.final a✝ ∼ StrictMember.final ⋯
no goals