entails — B follows from its incoming input(s); converging arrows are joint unless the node describes alternate routes
discharges — A proves away assumption B
rests on — B is an assumption needed by A (an in-Lean hypothesis, or an out-of-Lean floor)
Proven theorem
Hypothesis in statement
Out-of-Lean assumption
Definition — a claim (Prop) or construction (data)
Top-level result (verifier soundness)