case mp reactor =>
  simp only [triggers.activated, reactionInputs]
  cases hp : reaction.subPS.coe p'
  case inl loc =>
    simp
    cases he
    case input hi =>
      simp [hi] at hp
      cases h
      case port h =>
        simp [portIsPresent, hp] at h
        exact h
    case output ho =>
      rw [ho] at hp
      contradiction
  case inr sub =>
    have ⟨c, output⟩ := sub
    simp at output ⊢
    cases he
    case input hi =>
      rw [hi] at hp
      contradiction
    case output c' output' ho =>
      simp [ho] at hp
      injection hp with hc ho
      subst hc
      subst ho
      cases h
      case port h =>
        simp [portIsPresent] at h
        have ⟨v, hv⟩ := h
        exists cast sorry v
        simp [hv]
        sorry
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
⊢ Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
no goals