case neg =>
  have hv₁ := wf.valid_deps hc₁ hr₁ hd₁
  have hv₂ := wf.valid_deps hc₂ hr₂ hd₂
  cases k <;> cases cpt <;> try cases ‹Kind› 
  have := obj?_some_extend hc₁ hr₁
  case out.inp => 
    have hd₂' := wf.unique_inputs (obj?_some_extend hc₁ hr₁) (obj?_some_extend hc₂ hr₂) hi hd₁
    exact absurd hd₂ hd₂'
  case in.out =>
    cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
    case _ hn₁ hj₁ _ _ hn₂ hj₂ =>
      have hc₁' := obj?_some_extend hc₁ hn₁
      have hc₂' := obj?_some_extend hc₂ hn₂
      have hj := mem_get?_rtr_eq hc₁' hc₂' hj₁ hj₂
      injection hj with hj
      exact get?_some_rtr_eq hc₁ hc₂ (hj ▸ hn₁) hn₂ 
  all_goals 
    cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
    all_goals exact mem_get?_rtr_eq hc₁ hc₂ ‹_› ‹_›
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k : Kind
cpt : Component.Valued
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
⊢ c₁ = c₂
no goals