Theorem: Execution.Instantaneous.Step.seq_rcn_ne (ReactorModel/Execution/Theorems/Grouped/Instantaneous.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
⊢ rcn e₁ ≠ rcn e₂
Tactic:
by_contra he
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
he : rcn e₁ = rcn e₂
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
he : rcn e₁ = rcn e₂
⊢ False
Tactic:
exact e₂.allows_rcn.unprocessed (he ▸ e₁.rcn_mem_progress)
State after:
no goals