QHT is a first-order super-intuitionistic logic that provides a foundation for answer set programming (ASP) and a useful tool for analysing and transforming non-ground programs. We recall some properties of QHT and its nonmonotonic extension, quantified equilibrium logic (QEL). We show how the proof theory of QHT can be used to extend to non-ground programs previous results on the completeness of θ-subsumption. We also establish a reduction of QHT to classical logic and show how this can be used to obtain and extend classical encodings for concepts such as the strong equivalence of programs and theories. We pay special attention to a class of general (disjunctive) logic programs that capture all universal theories in QEL.