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

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ᵢ s₂
⊢ s₁.progress ⊂ s₂.progress
Tactic:
simp [e.progress_eq, Set.ssubset_iff_insert]
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ᵢ s₂
⊢ ∃ a ∉ s₁.progress, insert a s₁.progress ⊆ Set.insert (rcn e) s₁.progress

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ᵢ s₂
⊢ ∃ a ∉ s₁.progress, insert a s₁.progress ⊆ Set.insert (rcn e) s₁.progress
Tactic:
exists e.rcn, e.allows_rcn.unprocessed
State after:
no goals