constructor <;> intro ⟨hd, hp⟩
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
⊢ dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress ↔
    dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress
case mp
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress

case mpr
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
hp : i₂ ∉ Set.insert i₁ s.progress
⊢ dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress