Lemma invert_type_App `{checker_flags} Σ Γ f u T :
  Σ ;;; Γ |- tApp f u : T →
  { T' : term & { U' & ((Σ ;;; Γ |- f : T') × typing_spine Σ Γ T' u U' ×
                        (isApp f = false) × (u ≠ []) ×
                        (Σ ;;; Γ |- U' ≤ T))%type } }.

Lemma type_mkApp `{checker_flags} Σ Γ f u T T' :
  Σ ;;; Γ |- f : T →
  typing_spine Σ Γ T [u] T' →
  Σ ;;; Γ |- mkApp f u : T'.

Lemma type_mkApps `{checker_flags} Σ Γ f u T T' :
  Σ ;;; Γ |- f : T →
  typing_spine Σ Γ T u T' →
  Σ ;;; Γ |- mkApps f u : T'.