subst ht
case norm
out : Output
t : Component.Valued × ID
a✝ : Change.Normal
hc : Change.norm a✝ ∈ out
ht : (a✝.cpt, a✝.id) = t
⊢ Change.Targets (Change.norm a✝) t.1 t.2
case norm
out : Output
a✝ : Change.Normal
hc : Change.norm a✝ ∈ out
⊢ Change.Targets (Change.norm a✝) (a✝.cpt, a✝.id).1 (a✝.cpt, a✝.id).2