Theorem: Execution.Step.Exec.unprocessed_ssubset (ReactorModel/Execution/Theorems/Step/Exec.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ unprocessed s₂ ⊂ unprocessed s₁
Tactic:
simp [e.unprocessed_eq, Set.ssubset_iff_subset_ne]
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ rcn e ∈ unprocessed s₁

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ rcn e ∈ unprocessed s₁
Tactic:
exact e.rcn_mem_unprocessed
State after:
no goals