split <;> (constructor; assumption)
case port
net : Network
reactor : ReactorId net
reaction : Reaction (Path.class reactor)
p✝ : reaction.val.portSources.vars
⊢ (match Interface.Subscheme.coe p✝ with
    | Sum.inl input => port { reactor := reactor, port := input }
    | 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✝
no goals