Fixpoint lift n k t : term :=
  match t with
  | tRel i ⇒ if Nat.leb k i then tRel (n + i) else tRel i
  | tEvar ev args ⇒ tEvar ev (List.map (lift n k) args)
  | tLambda na M ⇒ tLambda na (lift n (S k) M)
  | tApp u v ⇒ tApp (lift n k u) (lift n k v)
  | tLetIn na b b' ⇒ tLetIn na (lift n k b) (lift n (S k) b')
  | tCase ind c brs ⇒
    let brs' := List.map (on_snd (lift n k)) brs in
    tCase ind (lift n k c) brs'
  | tProj p c ⇒ tProj p (lift n k c)
  | tFix mfix idx ⇒
    let k' := List.length mfix + k in
    let mfix' := List.map (map_def (lift n k')) mfix in
    tFix mfix' idx
  | tCoFix mfix idx ⇒
    let k' := List.length mfix + k in
    let mfix' := List.map (map_def (lift n k')) mfix in
    tCoFix mfix' idx
  | tBox ⇒ t
  | tVar _ ⇒ t
  | tConst _ ⇒ t
  | tConstruct _ _ ⇒ t
  end.

Notation lift0 n := (lift n 0).
Definition up := lift 1 0.

Fixpoint subst s k u :=
  match u with
  | tRel n ⇒
    if Nat.leb k n then
      match nth_error s (n - k) with
      | Some b ⇒ lift0 k b
      | None ⇒ tRel (n - List.length s)
      end
    else tRel n
  | tEvar ev args ⇒ tEvar ev (List.map (subst s k) args)
  | tLambda na M ⇒ tLambda na (subst s (S k) M)
  | tApp u v ⇒ tApp (subst s k u) (subst s k v)
  | tLetIn na b b' ⇒ tLetIn na (subst s k b) (subst s (S k) b')
  | tCase ind c brs ⇒
    let brs' := List.map (on_snd (subst s k)) brs in
    tCase ind (subst s k c) brs'
  | tProj p c ⇒ tProj p (subst s k c)
  | tFix mfix idx ⇒
    let k' := List.length mfix + k in
    let mfix' := List.map (map_def (subst s k')) mfix in
    tFix mfix' idx
  | tCoFix mfix idx ⇒
    let k' := List.length mfix + k in
    let mfix' := List.map (map_def (subst s k')) mfix in
    tCoFix mfix' idx
  | x ⇒ x
  end.

Notation subst0 t := (subst t 0).
Definition subst1 t k u := subst [t] k u.
Notation subst10 t := (subst1 t 0).
Notation "M { j := N }" := (subst1 N j M) (at level 10, right associativity).

Fixpoint closedn k (t : term) : bool :=
  match t with
  | tRel i ⇒ Nat.ltb i k
  | tEvar ev args ⇒ List.forallb (closedn k) args
  | tLambda _ M ⇒ closedn (S k) M
  | tApp u v ⇒ closedn k u && closedn k v
  | tLetIn na b b' ⇒ closedn k b && closedn (S k) b'
  | tCase ind c brs ⇒
    let brs' := List.forallb (test_snd (closedn k)) brs in
    closedn k c && brs'
  | tProj p c ⇒ closedn k c
  | tFix mfix idx ⇒
    let k' := List.length mfix + k in
    List.forallb (test_def (closedn k')) mfix
  | tCoFix mfix idx ⇒
    let k' := List.length mfix + k in
    List.forallb (test_def (closedn k')) mfix
  | x ⇒ true
  end.

Notation closed t := (closedn 0 t).






Notation subst_rec N M k := (subst N k M) (only parsing).


Lemma lift_rel_ge :
  ∀ k n p, p ≤ n → lift k p (tRel n) = tRel (k + n).

Lemma lift_rel_lt : ∀ k n p, p > n → lift k p (tRel n) = tRel n.

Lemma lift_rel_alt : ∀ n k i, lift n k (tRel i) = tRel (if Nat.leb k i then n + i else i).

Lemma subst_rel_lt : ∀ u n k, k > n → subst u k (tRel n) = tRel n.

Lemma subst_rel_gt :
  ∀ u n k, n ≥ k + length u → subst u k (tRel n) = tRel (n - length u).

Lemma subst_rel_eq :
  ∀ (u : list term) n i t p,
    List.nth_error u i = Some t → p = n + i →
    subst u n (tRel p) = lift0 n t.


Lemma on_snd_eq_id_spec {A B} (f : B → B) (x : A × B) :
  f (snd x) = snd x ↔
  on_snd f x = x.

Lemma map_def_eq_spec (f g : term → term) (x : def term) :
  f (dbody x) = g (dbody x) →
  map_def f x = map_def g x.

Lemma map_def_id_spec (f : term → term) (x : def term) :
  f (dbody x) = (dbody x) →
  map_def f x = x.

Lemma compose_map_def (f g : term → term) :
  compose (map_def f) (map_def g) = map_def (compose f g).







Lemma lift0_id : ∀ M k, lift 0 k M = M.

Lemma lift0_p : ∀ M, lift0 0 M = M.




Lemma simpl_lift :
  ∀ M n k p i,
    i ≤ k + n →
    k ≤ i → lift p i (lift n k M) = lift (p + n) k M.

Lemma simpl_lift0 : ∀ M n, lift0 (S n) M = lift0 1 (lift0 n M).

Lemma permute_lift :
  ∀ M n k p i,
    i ≤ k →
    lift p i (lift n k M) = lift n (k + p) (lift p i M).

Lemma permute_lift0 :
  ∀ M k, lift0 1 (lift 1 k M) = lift 1 (S k) (lift0 1 M).

Lemma lift_isApp n k t : ¬ isApp t = true → ¬ isApp (lift n k t) = true.

Lemma map_non_nil {A B} (f : A → B) l : l ≠ nil → map f l ≠ nil.

Lemma isLambda_lift n k (bod : term) :
  isLambda bod = true → isLambda (lift n k bod) = true.



Lemma simpl_subst_rec :
  ∀ M N n p k,
    p ≤ n + k →
    k ≤ p → subst N p (lift (List.length N + n) k M) = lift n k M.

Lemma simpl_subst :
  ∀ N M n p, p ≤ n → subst N p (lift0 (length N + n) M) = lift0 n M.

Lemma lift_mkApps n k t l : lift n k (mkApps t l) = mkApps (lift n k t) (map (lift n k) l).

Lemma commut_lift_subst_rec :
  ∀ M N n p k,
    k ≤ p →
    lift n k (subst N p M) = subst N (p + n) (lift n k M).

Lemma commut_lift_subst :
  ∀ M N k, subst N (S k) (lift0 1 M) = lift0 1 (subst N k M).

Lemma distr_lift_subst_rec :
  ∀ M N n p k,
    lift n (p + k) (subst N p M) =
    subst (List.map (lift n k) N) p (lift n (p + length N + k) M).

Lemma distr_lift_subst :
  ∀ M N n k,
    lift n k (subst0 N M) = subst0 (map (lift n k) N) (lift n (length N + k) M).

Lemma distr_lift_subst10 :
  ∀ M N n k,
    lift n k (subst10 N M) = subst10 (lift n k N) (lift n (S k) M).

Lemma subst_mkApps u k t l :
  subst u k (mkApps t l) = mkApps (subst u k t) (map (subst u k) l).

Lemma subst1_mkApps u k t l : subst1 u k (mkApps t l) = mkApps (subst1 u k t) (map (subst1 u k) l).

Lemma distr_subst_rec :
  ∀ M N (P : list term) n p,
    subst P (p + n) (subst N p M) =
    subst (map (subst P n) N) p (subst P (p + length N + n) M).

Lemma distr_subst :
  ∀ P N M k,
    subst P k (subst0 N M) = subst0 (map (subst P k) N) (subst P (length N + k) M).

Lemma lift_closed n k t : closedn k t → lift n k t = t.

Lemma closed_upwards {k t} k' : closedn k t → k' ≥ k → closedn k' t.

Lemma subst_empty k a : subst [] k a = a.


Lemma simpl_subst_k (N : list term) (M : term) :
  ∀ k p, p = #|N| → subst N k (lift p k M) = M.

Lemma subst_app_decomp l l' k t :
  subst (l ++ l') k t = subst l' k (subst (List.map (lift0 (length l')) l) k t).

Lemma subst_app_simpl l l' k t :
  subst (l ++ l') k t = subst l k (subst l' (k + length l) t).

Lemma isLambda_subst (s : list term) k (bod : term) :
  isLambda bod = true → isLambda (subst s k bod) = true.