constructor
case port.h_2
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✝ }
⊢ port
      { reactor := Path.extend reactor c✝,
        port :=
          cast
            (_ :
              ((fun child => interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars =
                (interface (Path.class (Path.extend reactor c✝))
                    (match Reactor.PortKind.output with
                    | Reactor.PortKind.input => Reactor.InterfaceKind.inputs
                    | Reactor.PortKind.output => Reactor.InterfaceKind.outputs)).vars)
            output✝ } ≡
    _root_.Trigger.port p✝
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✝ }