Fixpoint wf_Inv (t : term) :=
  match t with
  | tRel _ | tVar _ | tSort _ ⇒ True
  | tEvar n l ⇒ Forall wf l
  | tCast t k t' ⇒ wf t ∧ wf t'
  | tProd na t b ⇒ wf t ∧ wf b
  | tLambda na t b ⇒ wf t ∧ wf b
  | tLetIn na t b b' ⇒ wf t ∧ wf b ∧ wf b'
  | tApp t u ⇒ isApp t = false ∧ u ≠ nil ∧ wf t ∧ Forall wf u
  | tConst _ _ | tInd _ _ | tConstruct _ _ _ ⇒ True
  | tCase ci p c brs ⇒ wf p ∧ wf c ∧ Forall (Program.Basics.compose wf snd) brs
  | tProj p t ⇒ wf t
  | tFix mfix k ⇒ Forall (fun def ⇒ wf def.(dtype) ∧ wf def.(dbody) ∧ isLambda def.(dbody) = true) mfix
  | tCoFix mfix k ⇒ Forall (fun def ⇒ wf def.(dtype) ∧ wf def.(dbody)) mfix
  end.

Lemma wf_inv t (w : Ast.wf t) : wf_Inv t.

Lemma decompose_app_mkApps f l :
  ~~ isApp f → decompose_app (mkApps f l) = (f, l).

Lemma atom_decompose_app t : ~~ isApp t → decompose_app t = (t, []).

Lemma mkApps_eq_inj {t t' l l'} :
  mkApps t l = mkApps t' l' →
  ~~ isApp t → ~~ isApp t' → t = t' ∧ l = l'.

Inductive mkApps_spec : term → list term → term → list term → term → Type :=
| mkApps_intro f l n :
    ~~ isApp f →
    mkApps_spec f l (mkApps f (firstn n l)) (skipn n l) (mkApps f l).

Lemma firstn_add {A} x y (args : list A) : firstn (x + y) args = firstn x args ++ firstn y (skipn x args).
Definition is_empty {A} (l : list A) :=
  if l is nil then true else false.

Lemma is_empty_app {A} (l l' : list A) : is_empty (l ++ l') = is_empty l && is_empty l'.

Fixpoint wf_term (t : term) : bool :=
  match t with
  | tRel _ | tVar _ ⇒ true
  | tEvar n l ⇒ forallb wf_term l
  | tSort u ⇒ true
  | tCast t k t' ⇒ wf_term t && wf_term t'
  | tProd na t b ⇒ wf_term t && wf_term b
  | tLambda na t b ⇒ wf_term t && wf_term b
  | tLetIn na t b b' ⇒ wf_term t && wf_term b && wf_term b'
  | tApp t u ⇒ ~~ isApp t && ~~ is_empty u && wf_term t && forallb wf_term u
  | tConst _ _ | tInd _ _ | tConstruct _ _ _ ⇒ true
  | tCase ci p c brs ⇒ wf_term p && wf_term c && forallb (Program.Basics.compose wf_term snd) brs
  | tProj p t ⇒ wf_term t
  | tFix mfix k ⇒
    forallb (fun def ⇒ wf_term def.(dtype) && wf_term def.(dbody) && isLambda def.(dbody)) mfix
  | tCoFix mfix k ⇒
    forallb (fun def ⇒ wf_term def.(dtype) && wf_term def.(dbody)) mfix
  end.

Lemma mkApps_tApp f args :
  ~~ isApp f →
  ~~ is_empty args →
  tApp f args = mkApps f args.

Lemma decompose_app_inv' f l hd args : wf_term f →
                                       decompose_app (mkApps f l) = (hd, args) →
                                       ∑ n, ~~ isApp hd ∧ l = skipn n args ∧ f = mkApps hd (firstn n args).

Lemma mkApps_elim t l : wf_term t →
                        let app' := decompose_app (mkApps t l) in
                        mkApps_spec app'.1 app'.2 t l (mkApps t l).

Lemma nApp_mkApps {t l} : ~~ isApp (mkApps t l) → ~~ isApp t ∧ l = [].

Lemma mkApps_nisApp {t t' l} : mkApps t l = t' → ~~ isApp t' → t = t' ∧ l = [].