  We show normalisation and decidability of convertibility for a type theory
with a hierarchy of universes and a proof irrelevant type of propositions,
close to the type system used in the proof assistant Lean. Contrary to previous
arguments, the proof does not require explicitly to introduce a notion of
neutral and normal forms.
