Is there a published strong normalisation proof for F omega extended with coproduct types and commuting conversions? Sam -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.