Longer Derivations

Assumptions inside assumptions, discharged in the order that nesting requires