apply List.forall_iff_forall_mem.mpr
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
⊢ List.Forall (fun x => ¬Change.Targets x cpt i) (output s i₁)
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
⊢ ∀ x ∈ output s i₁, ¬Change.Targets x cpt i