simp [List.perm_ext_iff_of_nodup e₁.rcns_nodup e₂.rcns_nodup, e₁.mem_rcns_iff, e₂.mem_rcns_iff]
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
e₁ : s ↓ᵢ| s₁
e₂ : s ↓ᵢ| s₂
⊢ rcns e₁ ~ rcns e₂
no goals