assumption
case port.h_2.a
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
x✝ : (reactionInputScheme (Path.class reactor)).vars
c✝ : Child (Path.class reactor)
output✝ : ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
heq✝ : Interface.Subscheme.coe p✝ = Sum.inr { fst := c✝, snd := output✝ }
⊢ Interface.Subscheme.coe p✝ = Sum.inr { fst := c✝, snd := output✝ }
no goals