Which interesting HA proofs can I run thorough the Dialectica translations to get non-trivial System T programs? I can do somewhat boring stuff like forall x. exists y. y = 2x, but is there something cooler and still compact?