Theorem: Execution.Step.Skip.equiv (ReactorModel/Execution/Theorems/Step/Skip.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ s₁.rtr ≈ s₂.rtr
Tactic:
simp [e.dst_eq, State.record_preserves_rtr]
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ s₁.rtr ≈ s₁.rtr

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₛ s₂
⊢ s₁.rtr ≈ s₁.rtr
Tactic:
exact .refl _
State after:
no goals