The Formulae-as-Types Notion of Construction