simp_all [Dependency.Acyclic.iff_mem_acyclic, triv]
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
triv : rtr[Component.rcn] = ∅
⊢ Acyclic rtr
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
triv : rtr[Component.rcn] = ∅
⊢ ∀ i ∈ ∅, ¬i <[rtr] i