I follow up on some comments I made about Curry-Howard for first-order quantifiers in the previous episode.  Sheard's Omega language also mentioned (see links on his web page).  First-order quantifications turn into indexed types where the indices are not program expressions but come from another syntactic domain.