contradiction
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
hp : Sum.inr { fst := c✝, snd := output✝ } = Sum.inl loc
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
no goals