simp [portIsPresent] at h
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
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
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : portIsPresent exec { reactor := Path.extend reactor c', port := cast _ output' } = true
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
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
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v