Trying to work out the classical/intuitionistic thing for the first-order dependent case. In the course of doing this I've made what I think is the tallest prooftree I've ever made: 17 proof rules, no branching. It demonstrates that
cent(λq.q(λvw.v(λu.u(λry.w<r,λz.z(λx.y x)>))))
has type
C((Πx . A(x)) cont → Σx.(A(x) cont))