Lemma type_mkApps {cf : checker_flags} {Σ Γ t u T t_ty} :
  (Σ ;;; Γ |- t : t_ty) ->
  typing_spine Σ Γ t_ty u T ->
  Σ ;;; Γ |- mkApps t u : T.
Proof.
  destruct 2; cbn; trivial.
  destruct ?; subst.
  all: try solve [ do 3 try first [ eassumption
                                  | reflexivity
                                  | congruence
                                  | econstructor ] ];
    [ > ].
  match goal with
  | [ H : _;;; _ |- tApp ?f ?x : _ |- _ ;;; _ |- tApp ?f (?x ++ _) : _ ]
    => inversion H; subst
  end.
  { econstructor; try eassumption; try congruence.
    { match goal with |- ?x ++ _ :: _ <> [] => now destruct x end. }
    { shelve. (* ???
1 goal (ID 8037)

  cf : checker_flags
  Σ : global_env_ext
  Γ : context
  T, t2 : term
  args : list term
  X : Σ;;; Γ |- tApp t2 args : T
  hd : term
  tl : list term
  na : aname
  A, B : term
  s : Universe.t
  B' : term
  t0 : Σ;;; Γ |- tProd na A B : tSort s
  c : Σ;;; Γ |- T <= tProd na A B
  t1 : Σ;;; Γ |- hd : A
  X0 : typing_spine Σ Γ (B {0 := hd}) tl B'
  t_ty : term
  X1 : Σ;;; Γ |- t2 : t_ty
  H1 : isApp t2 = false
  H3 : args <> []
  X2 : typing_spine Σ Γ t_ty args T
  ============================
  typing_spine Σ Γ t_ty (args ++ hd :: tl) B'
 *) } }
  { econstructor; try eassumption; [ | | ].
    (* ???
3 focused goals (shelved: 3) (ID 11491)

  cf : checker_flags
  Σ : global_env_ext
  Γ : context
  T, t2 : term
  args : list term
  X : Σ;;; Γ |- tApp t2 args : T
  hd : term
  tl : list term
  na : aname
  A, B : term
  s : Universe.t
  B' : term
  t0 : Σ;;; Γ |- tProd na A B : tSort s
  c : Σ;;; Γ |- T <= tProd na A B
  t1 : Σ;;; Γ |- hd : A
  X0 : typing_spine Σ Γ (B {0 := hd}) tl B'
  A0 : term
  s0 : Universe.t
  X1 : Σ;;; Γ |- tApp t2 args : A0
  X2 : Σ;;; Γ |- T : tSort s0
  X3 : Σ;;; Γ |- A0 <= T
  ============================
  Σ;;; Γ |- tApp t2 (args ++ hd :: tl) : ?A

goal 2 (ID 11492) is:
 Σ;;; Γ |- B' : tSort ?s
goal 3 (ID 11493) is:
 Σ;;; Γ |- ?A <= B'
*)