Cone interface and hypothesis-ledger syntax

A later paper must fix one actual finite list $\mathsf{H}=(H_1,\dots ,H_r)$ before invoking its extraction theorem. The template below is not an assertion that eight hypotheses have been instantiated or satisfied.