simp at output ⊢
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)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inr { fst := c, snd := output }) =
    true
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)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v