all_goals cases e₁.deterministic e₂; exact e₁'.deterministic e₂'
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
e₁ : s₁✝ -[hd✝]→ s₂✝¹
ht : Disjoint (Reaction.Output.targets (hd✝ :: tl✝)) (Reaction.Output.targets [])
e₁' : 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 α
e₂ : s₁✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ 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✝))
e₁ : s✝ -[hd✝]→ s₂✝¹
e₁' : s₂✝¹ -[tl✝]→ s₁₂
s₂✝ : State α
e₂ : s✝ -[hd✝]→ s₂✝
e₂' : s₂✝ -[tl✝]→ s₂₁
⊢ s₁₂ = s₂₁
no goals