constructor <;> intro ⟨hm, hd, hu⟩
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
⊢ Allows s₁ i ↔ Allows s₂ i
case mp
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₁.rtr[Component.rcn]
hd : dependencies s₁.rtr i ⊆ s₁.progress
hu : i ∉ s₁.progress
⊢ Allows s₂ i

case mpr
α : Type
inst✝ : Hierarchical α
s s₁✝ s₂✝ : State α
i : ID
s₁ s₂ : State α
hr : s₁.rtr ≈ s₂.rtr
hp : autoParam (s₁.progress = s₂.progress) _auto✝
hm : i ∈ s₂.rtr[Component.rcn]
hd : dependencies s₂.rtr i ⊆ s₂.progress
hu : i ∉ s₂.progress
⊢ Allows s₁ i