intro h
net : Network
next : Next net
exec : Executable net
⊢ Next.for exec = some next → exec.tag < next.tag
net : Network
next : Next net
exec : Executable net
h : Next.for exec = some next
⊢ exec.tag < next.tag