Strong normalization and consistency for the calculus of constructions with a universe hierarchy

Problem statement

Notes: Strong normalization requires Girard's reducibility candidates, and the impredicative `Prop` rule `(s, prop, prop)` is what makes a naive induction on types fail. The three anti-vacuity guards require a nonempty typing relation and exercise polymorphic typing, `Typing.app`, beta reduction, and substitution. Mathlib does not provide the requested Lean theorem; earlier Coq mechanizations and semantic models of CC and CCω are acknowledged in the module documentation.

Source: Coquand and Huet, 'The calculus of constructions' (1988); Zhaohui Luo, 'An Extended Calculus of Constructions' (1990); Bruno Barras, 'Sets in Coq, Coq in Sets' (2010).

Informal solution: Use reducibility candidates in the style of Girard, extended to dependent types and the predicative universe hierarchy. A smaller λC rehearsal replaces the hierarchy by `Prop` and a top sort `Type 0`; it is a different typing relation, not literally the restriction of this CCω syntax to two sorts.

/--
Anti-vacuity guard: the polymorphic identity `λ (A : Prop). λ (x : A). x` has type
`Π (A : Prop). Π (x : A). A`. This is typable only because `Prop` is impredicative.
-/
theorem declaration uses `sorry`typing_polyId :
    Typing [] (.lam (.srt .prop) (.lam (.var 0) (.var 0)))
      (.pi (.srt .prop) (.pi (.var 0) (.var 1))) := sorry

/--
Anti-vacuity guard: applying the polymorphic identity to `False` exercises application typing.
Here `False` is encoded as `Π (P : Prop). P`.
-/
theorem declaration uses `sorry`typing_polyId_app :
    Typing []
      (.app
        (.lam (.srt .prop) (.lam (.var 0) (.var 0)))
        (.pi (.srt .prop) (.var 0)))
      (.pi (.pi (.srt .prop) (.var 0)) (.pi (.srt .prop) (.var 0))) := sorry

/-- Anti-vacuity guard: the same application takes its expected beta step. -/
theorem declaration uses `sorry`step_polyId_app :
    Step
      (.app
        (.lam (.srt .prop) (.lam (.var 0) (.var 0)))
        (.pi (.srt .prop) (.var 0)))
      (.lam (.pi (.srt .prop) (.var 0)) (.var 0)) := sorry

/-- Types are preserved by reduction. -/
theorem declaration uses `sorry`subject_reduction (Γ : List Tm) (t t' A : Tm) :
    Typing Γ t A → Step t t' → Typing Γ t' A := sorry

/-- Every well-typed term is strongly normalizing. -/
theorem declaration uses `sorry`strong_normalization (Γ : List Tm) (t A : Tm) :
    Typing Γ t A → SN t := sorry

/-- The system is logically consistent: `Π (P : Prop). P` is not inhabited. -/
theorem declaration uses `sorry`consistency : ¬ ∃ t : Tm, Typing [] t (.pi (.srt .prop) (.var 0)) := sorry