induction e₁ generalizing s₂ <;> cases e₁₂ <;> cases e₂ <;> cases e₂₁
α : Type
inst✝ : Proper α
s s₁ s₂ s₁₂ s₂₁ : State α
c : Change
out out₁ out₂ : Reaction.Output
ht : Disjoint (Reaction.Output.targets out₁) (Reaction.Output.targets out₂)
e₁ : s -[out₁]→ s₁
e₁₂ : s₁ -[out₂]→ s₁₂
e₂ : s -[out₂]→ s₂
e₂₁ : s₂ -[out₁]→ s₂₁
⊢ s₁₂ = s₂₁
case refl.refl.refl.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ : State α
c : Change
out out₁ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets [])
⊢ s₁₂ = s₁₂

case refl.trans.trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
s✝ : State α
hd✝ : Change
s₂✝¹ : State α
tl✝ : Reaction.Output
ht : Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (hd✝ :: tl✝))
a✝³ : s✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
a✝¹ : s✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case trans.refl.refl.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝ : Change
s₁✝ s₂✝¹ : State α
tl✝ : Reaction.Output
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
a✝² : s₂✝¹ -[tl✝]→ s₁₂
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝) (Reaction.Output.targets []) →
      s₁₂ -[[]]→ s₁₂ → s₂✝¹ -[[]]→ s₂ → s₂ -[tl✝]→ s₂₁ → s₁₂ = s₂₁
s₂✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁

case trans.trans.trans.trans
α : Type
inst✝ : Proper α
s s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd✝¹ : Change
s₁✝ s₂✝³ : State α
tl✝¹ : Reaction.Output
s₃✝ : State α
a✝⁷ : s₁✝ -[hd✝¹]→ s₂✝³
a✝⁶ : s₂✝³ -[tl✝¹]→ s₃✝
s₂ : State α
hd✝ : Change
s₂✝² : State α
tl✝ : Reaction.Output
a_ih✝ :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl✝¹) (Reaction.Output.targets (hd✝ :: tl✝)) →
      s₃✝ -[hd✝ :: tl✝]→ s₁₂ → s₂✝³ -[hd✝ :: tl✝]→ s₂ → s₂ -[tl✝¹]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd✝¹ :: tl✝¹)) (Reaction.Output.targets (hd✝ :: tl✝))
a✝⁵ : s₃✝ -[hd✝]→ s₂✝²
a✝⁴ : s₂✝² -[tl✝]→ s₁₂
s₂✝¹ : State α
a✝³ : s₁✝ -[hd✝]→ s₂✝¹
a✝² : s₂✝¹ -[tl✝]→ s₂
s₂✝ : State α
a✝¹ : s₂ -[hd✝¹]→ s₂✝
a✝ : s₂✝ -[tl✝¹]→ s₂₁
⊢ s₁₂ = s₂₁