congr
case refl.refl.refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ record (record z₁₂ rcn₂) rcn₁ = record (record z₂₁ rcn₂) rcn₁
case refl.refl.refl.refl.e_s.e_s
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
rcn₁ : ID
s₁ : State α
a✝⁷ : Allows s rcn₁
a✝⁶ : Triggers s rcn₁
a₁ : s -[output s rcn₁]→ s₁
rcn₂ : ID
a✝⁵ : Allows (record s₁ rcn₁) rcn₂
a✝⁴ : Triggers (record s₁ rcn₁) rcn₂
s₂ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
z₁₂ : State α
f₁₂ : s₁ -[output s rcn₂]→ z₁₂
z₂₁ : State α
f₂₁ : s₂ -[output s rcn₁]→ z₂₁
a₁₂ : (record s₁ rcn₁) -[output s rcn₂]→ (record z₁₂ rcn₁)
a₂₁ : (record s₂ rcn₂) -[output s rcn₁]→ (record z₂₁ rcn₂)
⊢ z₁₂ = z₂₁