induction u <;> constructor
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ rtr₁ ≈ rtr₂
case final.mem_get?_iff
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}

case final.get?_rcn_some_eq
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂

case final.get?_rtr_some_equiv
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂

case nested.mem_get?_iff
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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✝ : n₁✝ ≈ n₂✝
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}

case nested.get?_rcn_some_eq
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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✝ : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂

case nested.get?_rtr_some_equiv
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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✝ : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂