Library Term

Require Import Arith.
Require Export Compare_dec.
Require Export Relations.

Hint Resolve t_step rt_step rt_refl: core.
Hint Unfold transp: core.

Section Termes.

  Inductive sort : Set :=
    | kind : sort
    | prop : sort.

  Inductive term : Set :=
    | Srt : sort -> term
    | Ref : nat -> term
    | Abs : term -> term -> term
    | App : term -> term -> term
    | Prod : term -> term -> term.

  Fixpoint lift_rec (n : nat) (t : term) (k : nat) {struct t} : term :=
    match t with
    | Srt s => Srt s
    | Ref i =>
        match le_gt_dec k i with
        | left _ => Ref (n + i)
        | right _ => Ref i
        end
    | Abs T M => Abs (lift_rec n T k) (lift_rec n M (S k))
    | App u v => App (lift_rec n u k) (lift_rec n v k)
    | Prod A B => Prod (lift_rec n A k) (lift_rec n B (S k))
    end.

  Definition lift n t := lift_rec n t 0.

  Fixpoint subst_rec (N M : term) (k : nat) {struct M} : term :=
    match M with
    | Srt s => Srt s
    | Ref i =>
        match lt_eq_lt_dec k i with
        | inleft (left _) => Ref (pred i)
        | inleft (right _) => lift k N
        | inright _ => Ref i
        end
    | Abs A B => Abs (subst_rec N A k) (subst_rec N B (S k))
    | App u v => App (subst_rec N u k) (subst_rec N v k)
    | Prod T U => Prod (subst_rec N T k) (subst_rec N U (S k))
    end.

  Definition subst N M := subst_rec N M 0.

  Inductive subterm : term -> term -> Prop :=
    | sbtrm_abs_l : ∀ A B, subterm A (Abs A B)
    | sbtrm_abs_r : ∀ A B, subterm B (Abs A B)
    | sbtrm_app_l : ∀ A B, subterm A (App A B)
    | sbtrm_app_r : ∀ A B, subterm B (App A B)
    | sbtrm_prod_l : ∀ A B, subterm A (Prod A B)
    | sbtrm_prod_r : ∀ A B, subterm B (Prod A B).

  Inductive mem_sort (s : sort) : term -> Prop :=
    | mem_eq : mem_sort s (Srt s)
    | mem_prod_l : ∀ u v, mem_sort s u -> mem_sort s (Prod u v)
    | mem_prod_r : ∀ u v, mem_sort s v -> mem_sort s (Prod u v)
    | mem_abs_l : ∀ u v, mem_sort s u -> mem_sort s (Abs u v)
    | mem_abs_r : ∀ u v, mem_sort s v -> mem_sort s (Abs u v)
    | mem_app_l : ∀ u v, mem_sort s u -> mem_sort s (App u v)
    | mem_app_r : ∀ u v, mem_sort s v -> mem_sort s (App u v).

End Termes.

  Hint Constructors subterm.
  Hint Constructors mem_sort.

Section Beta_Reduction.

  Inductive red1 : term -> term -> Prop :=
    | beta : ∀ M N T, red1 (App (Abs T M) N) (subst N M)
    | abs_red_l :
        ∀ M M', red1 M M' -> ∀ N, red1 (Abs M N) (Abs M' N)
    | abs_red_r :
        ∀ M M', red1 M M' -> ∀ N, red1 (Abs N M) (Abs N M')
    | app_red_l :
        ∀ M1 N1, red1 M1 N1 -> ∀ M2, red1 (App M1 M2) (App N1 M2)
    | app_red_r :
        ∀ M2 N2, red1 M2 N2 -> ∀ M1, red1 (App M1 M2) (App M1 N2)
    | prod_red_l :
        ∀ M1 N1, red1 M1 N1 -> ∀ M2, red1 (Prod M1 M2) (Prod N1 M2)
    | prod_red_r :
        ∀ M2 N2, red1 M2 N2 -> ∀ M1, red1 (Prod M1 M2) (Prod M1 N2).

  Inductive red (M : term) : term -> Prop :=
    | refl_red : red M M
    | trans_red : ∀ P N, red M P -> red1 P N -> red M N.

  Inductive conv (M : term) : term -> Prop :=
    | refl_conv : conv M M
    | trans_conv_red : ∀ P N, conv M P -> red1 P N -> conv M N
    | trans_conv_exp : ∀ P N, conv M P -> red1 N P -> conv M N.

  Inductive par_red1 : term -> term -> Prop :=
    | par_beta :
        ∀ M M' N N' T,
        par_red1 M M' ->
        par_red1 N N' -> par_red1 (App (Abs T M) N) (subst N' M')
    | sort_par_red : ∀ s, par_red1 (Srt s) (Srt s)
    | ref_par_red : ∀ n, par_red1 (Ref n) (Ref n)
    | abs_par_red :
        ∀ M M' T T',
        par_red1 M M' -> par_red1 T T' -> par_red1 (Abs T M) (Abs T' M')
    | app_par_red :
        ∀ M M' N N',
        par_red1 M M' -> par_red1 N N' -> par_red1 (App M N) (App M' N')
    | prod_par_red :
        ∀ M M' N N',
        par_red1 M M' -> par_red1 N N' -> par_red1 (Prod M N) (Prod M' N').

  Definition par_red := clos_trans term par_red1.

End Beta_Reduction.

  Hint Constructors red1: coc.
  Hint Constructors par_red1: coc.
  Hint Resolve refl_red refl_conv: coc.
  Hint Unfold par_red: coc.

Section Normalisation_Forte.

  Definition normal t := ∀ u, ~ red1 t u.

  Definition sn := Acc (transp _ red1).

End Normalisation_Forte.

  Hint Unfold sn: coc.

  Lemma eqterm : ∀ u v : term, {u = v} + {u <> v}.
Proof.
decide equality.
decide equality.

apply eq_nat_dec.
Qed.

  Lemma inv_lift_sort : ∀ s n t k, lift_rec n t k = Srt s -> t = Srt s.
intros.
destruct t; try discriminate H.
 auto.
 unfold lift_rec in H.
   destruct (le_gt_dec k n0); discriminate H.
Qed.

  Lemma inv_subst_sort :
    ∀ s x t k, subst_rec x t k = Srt s -> t = Srt s \/ x = Srt s.
intros.
destruct t; try discriminate H.
 auto.
 unfold subst_rec in H.
   destruct (lt_eq_lt_dec k n) as [[fv| eqv]| bv]; try discriminate H.
   right.
   unfold lift in H.
   apply inv_lift_sort with (1 := H).
Qed.

  Lemma lift_ref_ge :
   ∀ k n p, p <= n -> lift_rec k (Ref n) p = Ref (k + n).
intros; simpl in |- *.
elim (le_gt_dec p n); auto with arith.
intro; absurd (p <= n); auto with arith.
Qed.

  Lemma lift_ref_lt : ∀ k n p, p > n -> lift_rec k (Ref n) p = Ref n.
intros; simpl in |- *.
elim (le_gt_dec p n); auto with arith.
intro; absurd (p <= n); auto with arith.
Qed.

  Lemma subst_ref_lt : ∀ u n k, k > n -> subst_rec u (Ref n) k = Ref n.
simpl in |- *; intros.
elim (lt_eq_lt_dec k n); intros; auto with arith.
elim a; intros.
absurd (k <= n); auto with arith.

inversion_clear b in H.
elim gt_irrefl with n; auto with arith.
Qed.

  Lemma subst_ref_gt :
   ∀ u n k, n > k -> subst_rec u (Ref n) k = Ref (pred n).
simpl in |- *; intros.
elim (lt_eq_lt_dec k n); intros.
elim a; intros; auto with arith.
inversion_clear b in H.
elim gt_irrefl with n; auto with arith.

absurd (k <= n); auto with arith.
Qed.

  Lemma subst_ref_eq : ∀ u n, subst_rec u (Ref n) n = lift n u.
intros; simpl in |- *.
elim (lt_eq_lt_dec n n); intros.
elim a; intros; auto with coc.
elim lt_irrefl with n; auto with coc.

elim gt_irrefl with n; auto with coc.
Qed.

  Lemma lift_rec0 : ∀ M k, lift_rec 0 M k = M.
simple induction M; simpl in |- *; intros; auto with coc.
elim (le_gt_dec k n); auto with coc.

rewrite H; rewrite H0; auto with coc.

rewrite H; rewrite H0; auto with coc.

rewrite H; rewrite H0; auto with coc.
Qed.

  Lemma lift0 : ∀ M, lift 0 M = M.
intros; unfold lift in |- *.
apply lift_rec0; auto with coc.
Qed.

  Lemma simpl_lift_rec :
   ∀ M n k p i,
   i <= k + n ->
   k <= i -> lift_rec p (lift_rec n M k) i = lift_rec (p + n) M k.
simple induction M; simpl in |- *; intros; auto with coc.
elim (le_gt_dec k n); intros.
rewrite lift_ref_ge; auto with coc.
rewrite plus_assoc; auto with coc.

rewrite plus_comm.
apply le_trans with (k + n0); auto with arith.

rewrite lift_ref_lt; auto with arith.
apply le_gt_trans with k; auto with arith.

rewrite H; auto with arith; rewrite H0; simpl in |- *; auto with arith.

rewrite H; auto with arith; rewrite H0; simpl in |- *; auto with arith.

rewrite H; auto with arith; rewrite H0; simpl in |- *; auto with arith.
Qed.

  Lemma simpl_lift : ∀ M n, lift (S n) M = lift 1 (lift n M).
intros; unfold lift in |- *.
rewrite simpl_lift_rec; auto with arith.
Qed.

  Lemma permute_lift_rec :
   ∀ M n k p i,
   i <= k ->
   lift_rec p (lift_rec n M k) i = lift_rec n (lift_rec p M i) (p + k).
simple induction M; simpl in |- *; intros; auto with coc.
elim (le_gt_dec k n); elim (le_gt_dec i n); intros.
rewrite lift_ref_ge; auto with arith.
rewrite lift_ref_ge; auto with arith.
elim plus_assoc_reverse with p n0 n.
elim plus_assoc_reverse with n0 p n.
elim plus_comm with p n0; auto with arith.

apply le_trans with n; auto with arith.

absurd (i <= n); auto with arith.
apply le_trans with k; auto with arith.

rewrite lift_ref_ge; auto with arith.
rewrite lift_ref_lt; auto with arith.

rewrite lift_ref_lt; auto with arith.
rewrite lift_ref_lt; auto with arith.
apply le_gt_trans with k; auto with arith.

rewrite H; auto with arith; rewrite H0; auto with arith.
rewrite plus_n_Sm; auto with arith.

rewrite H; auto with arith; rewrite H0; auto with arith.

rewrite H; auto with arith; rewrite H0; auto with arith.
rewrite plus_n_Sm; auto with arith.
Qed.

  Lemma permute_lift :
   ∀ M k, lift 1 (lift_rec 1 M k) = lift_rec 1 (lift 1 M) (S k).
intros.
change (lift_rec 1 (lift_rec 1 M k) 0 = lift_rec 1 (lift_rec 1 M 0) (1 + k))
 in |- *.
apply permute_lift_rec; auto with arith.
Qed.

  Lemma simpl_subst_rec :
   ∀ N M n p k,
   p <= n + k ->
   k <= p -> subst_rec N (lift_rec (S n) M k) p = lift_rec n M k.
simple induction M; simpl in |- *; intros; auto with arith.
elim (le_gt_dec k n); intros.
rewrite subst_ref_gt; auto with arith.
red in |- *; red in |- *.
apply le_trans with (S (n0 + k)); auto with arith.

rewrite subst_ref_lt; auto with arith.
apply le_gt_trans with k; auto with arith.

rewrite H; auto with arith; rewrite H0; auto with arith.
elim plus_n_Sm with n k; auto with arith.

rewrite H; auto with arith; rewrite H0; auto with arith.

rewrite H; auto with arith; rewrite H0; auto with arith.
elim plus_n_Sm with n k; auto with arith.
Qed.

  Lemma simpl_subst :
   ∀ N M n p, p <= n -> subst_rec N (lift (S n) M) p = lift n M.
intros; unfold lift in |- *.
apply simpl_subst_rec; auto with arith.
Qed.

  Lemma commut_lift_subst_rec :
   ∀ M N n p k,
   k <= p ->
   lift_rec n (subst_rec N M p) k = subst_rec N (lift_rec n M k) (n + p).
simple induction M; intros; auto with arith.
unfold subst_rec at 1, lift_rec at 2 in |- *.
elim (lt_eq_lt_dec p n); elim (le_gt_dec k n); intros.
elim a0.
case n; intros.
inversion_clear a1.

unfold pred in |- *.
rewrite lift_ref_ge; auto with arith.
rewrite subst_ref_gt; auto with arith.
elim plus_n_Sm with n0 n1.
auto with arith.

apply le_trans with p; auto with arith.

simple induction 1.
rewrite subst_ref_eq.
unfold lift in |- *.
rewrite simpl_lift_rec; auto with arith.

absurd (k <= n); auto with arith.
apply le_trans with p; auto with arith.
elim a; auto with arith.
simple induction 1; auto with arith.

rewrite lift_ref_ge; auto with arith.
rewrite subst_ref_lt; auto with arith.

rewrite lift_ref_lt; auto with arith.
rewrite subst_ref_lt; auto with arith.
apply le_gt_trans with p; auto with arith.

simpl in |- *.
rewrite plus_n_Sm.
rewrite H; auto with arith; rewrite H0; auto with arith.

simpl in |- *; rewrite H; auto with arith; rewrite H0; auto with arith.

simpl in |- *; rewrite plus_n_Sm.
rewrite H; auto with arith; rewrite H0; auto with arith.
Qed.

  Lemma commut_lift_subst :
   ∀ M N k, subst_rec N (lift 1 M) (S k) = lift 1 (subst_rec N M k).
intros; unfold lift in |- *.
rewrite commut_lift_subst_rec; auto with arith.
Qed.

  Lemma distr_lift_subst_rec :
   ∀ M N n p k,
   lift_rec n (subst_rec N M p) (p + k) =
   subst_rec (lift_rec n N k) (lift_rec n M (S (p + k))) p.
simple induction M; intros; auto with arith.
unfold subst_rec at 1 in |- *.
elim (lt_eq_lt_dec p n); intro.
elim a.
case n; intros.
inversion_clear a0.

unfold pred, lift_rec at 1 in |- *.
elim (le_gt_dec (p + k) n1); intro.
rewrite lift_ref_ge; auto with arith.
elim plus_n_Sm with n0 n1.
rewrite subst_ref_gt; auto with arith.
red in |- *; red in |- *; apply le_n_S.
apply le_trans with (n0 + (p + k)); auto with arith.
apply le_trans with (p + k); auto with arith.

rewrite lift_ref_lt; auto with arith.
rewrite subst_ref_gt; auto with arith.

simple induction 1.
unfold lift in |- *.
rewrite <- permute_lift_rec; auto with arith.
rewrite lift_ref_lt; auto with arith.
rewrite subst_ref_eq; auto with arith.

rewrite lift_ref_lt; auto with arith.
rewrite lift_ref_lt; auto with arith.
rewrite subst_ref_lt; auto with arith.

simpl in |- *; replace (S (p + k)) with (S p + k); auto with arith.
rewrite H; rewrite H0; auto with arith.

simpl in |- *; rewrite H; rewrite H0; auto with arith.

simpl in |- *; replace (S (p + k)) with (S p + k); auto with arith.
rewrite H; rewrite H0; auto with arith.
Qed.

  Lemma distr_lift_subst :
   ∀ M N n k,
   lift_rec n (subst N M) k = subst (lift_rec n N k) (lift_rec n M (S k)).
intros; unfold subst in |- *.
pattern k at 1 3 in |- *.
replace k with (0 + k); auto with arith.
apply distr_lift_subst_rec.
Qed.

  Lemma distr_subst_rec :
   ∀ M N P n p,
   subst_rec P (subst_rec N M p) (p + n) =
   subst_rec (subst_rec P N n) (subst_rec P M (S (p + n))) p.
simple induction M; auto with arith; intros.
unfold subst_rec at 2 in |- *.
elim (lt_eq_lt_dec p n); intro.
elim a.
case n; intros.
inversion_clear a0.

unfold pred, subst_rec at 1 in |- *.
elim (lt_eq_lt_dec (p + n0) n1); intro.
elim a1.
case n1; intros.
inversion_clear a2.

rewrite subst_ref_gt; auto with arith.
rewrite subst_ref_gt; auto with arith.
apply gt_le_trans with (p + n0); auto with arith.

simple induction 1.
rewrite subst_ref_eq; auto with arith.
rewrite simpl_subst; auto with arith.

rewrite subst_ref_lt; auto with arith.
rewrite subst_ref_gt; auto with arith.

simple induction 1.
rewrite subst_ref_lt; auto with arith.
rewrite subst_ref_eq.
unfold lift in |- *.
rewrite commut_lift_subst_rec; auto with arith.

do 3 (rewrite subst_ref_lt; auto with arith).

simpl in |- *; replace (S (p + n)) with (S p + n); auto with arith.
rewrite H; auto with arith; rewrite H0; auto with arith.

simpl in |- *; rewrite H; rewrite H0; auto with arith.

simpl in |- *; replace (S (p + n)) with (S p + n); auto with arith.
rewrite H; rewrite H0; auto with arith.
Qed.

  Lemma distr_subst :
   ∀ P N M k,
   subst_rec P (subst N M) k = subst (subst_rec P N k) (subst_rec P M (S k)).
intros; unfold subst in |- *.
pattern k at 1 3 in |- *.
replace k with (0 + k); auto with arith.
apply distr_subst_rec.
Qed.

  Lemma one_step_red : ∀ M N, red1 M N -> red M N.
intros.
apply trans_red with M; auto with coc.
Qed.

  Hint Resolve one_step_red: coc.

  Lemma red1_red_ind :
   ∀ N P,
   (P:term -> Prop) N ->
   (∀ M R, red1 M R -> red R N -> P R -> P M) ->
   ∀ M, red M N -> P M.
cut
 (∀ M N,
  red M N ->
  ∀ P : term -> Prop,
  P N -> (∀ M R, red1 M R -> red R N -> P R -> P M) -> P M).
intros.
apply (H M N); auto with coc.

simple induction 1; intros; auto with coc.
apply H1; auto with coc.
apply H4 with N0; auto with coc.

intros.
apply H4 with R; auto with coc.
apply trans_red with P; auto with coc.
Qed.

  Lemma trans_red_red : ∀ M N P, red M N -> red N P -> red M P.
intros.
generalize H0 M H.
simple induction 1; auto with coc.
intros.
apply trans_red with P0; auto with coc.
Qed.

  Lemma red_red_app :
   ∀ u u0 v v0, red u u0 -> red v v0 -> red (App u v) (App u0 v0).
simple induction 1.
simple induction 1; intros; auto with coc.
apply trans_red with (App u P); auto with coc.

intros.
apply trans_red with (App P v0); auto with coc.
Qed.

  Lemma red_red_abs :
   ∀ u u0 v v0, red u u0 -> red v v0 -> red (Abs u v) (Abs u0 v0).
simple induction 1.
simple induction 1; intros; auto with coc.
apply trans_red with (Abs u P); auto with coc.

intros.
apply trans_red with (Abs P v0); auto with coc.
Qed.

  Lemma red_red_prod :
   ∀ u u0 v v0, red u u0 -> red v v0 -> red (Prod u v) (Prod u0 v0).
simple induction 1.
simple induction 1; intros; auto with coc.
apply trans_red with (Prod u P); auto with coc.

intros.
apply trans_red with (Prod P v0); auto with coc.
Qed.

  Hint Resolve red_red_app red_red_abs red_red_prod: coc.

  Lemma red1_lift :
   ∀ n u v, red1 u v -> ∀ k, red1 (lift_rec n u k) (lift_rec n v k).
simple induction 1; simpl in |- *; intros; auto with coc.
rewrite distr_lift_subst; auto with coc.
Qed.

  Hint Resolve red1_lift: coc.

  Lemma red1_subst_r :
   ∀ a t u,
   red1 t u -> ∀ k, red1 (subst_rec a t k) (subst_rec a u k).
simple induction 1; simpl in |- *; intros; auto with coc.
rewrite distr_subst; auto with coc.
Qed.

  Lemma red1_subst_l :
   ∀ t u,
   red1 t u -> ∀ a k, red (subst_rec t a k) (subst_rec u a k).
simple induction a; simpl in |- *; auto with coc.
intros.
elim (lt_eq_lt_dec k n); intros; auto with coc.
elim a0; auto with coc.
unfold lift in |- *; auto with coc.
Qed.

  Hint Resolve red1_subst_l red1_subst_r: coc.

  Lemma red_prod_prod :
   ∀ u v t,
   red (Prod u v) t ->
   ∀ P : Prop,
   (∀ a b, t = Prod a b -> red u a -> red v b -> P) -> P.
simple induction 1; intros.
apply H0 with u v; auto with coc.

apply H1; intros.
inversion_clear H4 in H2.
inversion H2.
apply H3 with N1 b; auto with coc.
apply trans_red with a; auto with coc.

apply H3 with a N2; auto with coc.
apply trans_red with b; auto with coc.
Qed.

  Lemma red_sort_sort : ∀ s t, red (Srt s) t -> t <> Srt s -> False.
simple induction 1; intros; auto with coc.
apply H1.
generalize H2.
case P; intros; try discriminate.
inversion_clear H4.
Qed.

  Lemma one_step_conv_exp : ∀ M N, red1 M N -> conv N M.
intros.
apply trans_conv_exp with N; auto with coc.
Qed.

  Lemma red_conv : ∀ M N, red M N -> conv M N.
simple induction 1; auto with coc.
intros; apply trans_conv_red with P; auto with coc.
Qed.

  Hint Resolve one_step_conv_exp red_conv: coc.

  Lemma sym_conv : ∀ M N, conv M N -> conv N M.
simple induction 1; auto with coc.
simple induction 2; intros; auto with coc.
apply trans_conv_red with P0; auto with coc.

apply trans_conv_exp with P0; auto with coc.

simple induction 2; intros; auto with coc.
apply trans_conv_red with P0; auto with coc.

apply trans_conv_exp with P0; auto with coc.
Qed.

  Hint Immediate sym_conv: coc.

  Lemma trans_conv_conv : ∀ M N P, conv M N -> conv N P -> conv M P.
intros.
generalize M H; elim H0; intros; auto with coc.
apply trans_conv_red with P0; auto with coc.

apply trans_conv_exp with P0; auto with coc.
Qed.

  Lemma conv_conv_prod :
   ∀ a b c d, conv a b -> conv c d -> conv (Prod a c) (Prod b d).
intros.
apply trans_conv_conv with (Prod a d).
elim H0; intros; auto with coc.
apply trans_conv_red with (Prod a P); auto with coc.

apply trans_conv_exp with (Prod a P); auto with coc.

elim H; intros; auto with coc.
apply trans_conv_red with (Prod P d); auto with coc.

apply trans_conv_exp with (Prod P d); auto with coc.
Qed.

  Lemma conv_conv_lift :
   ∀ a b n k, conv a b -> conv (lift_rec n a k) (lift_rec n b k).
intros.
elim H; intros; auto with coc.
apply trans_conv_red with (lift_rec n P k); auto with coc.

apply trans_conv_exp with (lift_rec n P k); auto with coc.
Qed.

  Lemma conv_conv_subst :
   ∀ a b c d k,
   conv a b -> conv c d -> conv (subst_rec a c k) (subst_rec b d k).
intros.
apply trans_conv_conv with (subst_rec a d k).
elim H0; intros; auto with coc.
apply trans_conv_red with (subst_rec a P k); auto with coc.

apply trans_conv_exp with (subst_rec a P k); auto with coc.

elim H; intros; auto with coc.
apply trans_conv_conv with (subst_rec P d k); auto with coc.

apply trans_conv_conv with (subst_rec P d k); auto with coc.
apply sym_conv; auto with coc.
Qed.

  Hint Resolve conv_conv_prod conv_conv_lift conv_conv_subst: coc.

  Lemma refl_par_red1 : ∀ M, par_red1 M M.
simple induction M; auto with coc.
Qed.

  Hint Resolve refl_par_red1: coc.

  Lemma red1_par_red1 : ∀ M N, red1 M N -> par_red1 M N.
simple induction 1; auto with coc; intros.
Qed.

  Hint Resolve red1_par_red1: coc.

  Lemma red_par_red : ∀ M N, red M N -> par_red M N.
red in |- *; simple induction 1; intros; auto with coc.
apply t_trans with P; auto with coc.
Qed.

  Lemma par_red_red : ∀ M N, par_red M N -> red M N.
simple induction 1.
simple induction 1; intros; auto with coc.
apply trans_red with (App (Abs T M') N'); auto with coc.

intros.
apply trans_red_red with y; auto with coc.
Qed.

  Hint Resolve red_par_red par_red_red: coc.

  Lemma par_red1_lift :
   ∀ n a b,
   par_red1 a b -> ∀ k, par_red1 (lift_rec n a k) (lift_rec n b k).
simple induction 1; simpl in |- *; auto with coc.
intros.
rewrite distr_lift_subst; auto with coc.
Qed.

  Lemma par_red1_subst :
   ∀ a b c d,
   par_red1 a b ->
   par_red1 c d -> ∀ k, par_red1 (subst_rec a c k) (subst_rec b d k).
simple induction 2; simpl in |- *; auto with coc; intros.
rewrite distr_subst; auto with coc.

elim (lt_eq_lt_dec k n); auto with coc; intros.
elim a0; intros; auto with coc.
unfold lift in |- *.
apply par_red1_lift; auto with coc.
Qed.

  Lemma inv_par_red_abs :
   ∀ (P : Prop) T U x,
   par_red1 (Abs T U) x ->
   (∀ T' U', x = Abs T' U' -> par_red1 U U' -> P) -> P.
do 5 intro.
inversion_clear H; intros.
apply H with T' M'; auto with coc.
Qed.

  Hint Resolve par_red1_lift par_red1_subst: coc.

  Lemma mem_sort_lift :
   ∀ t n k s, mem_sort s (lift_rec n t k) -> mem_sort s t.
simple induction t; simpl in |- *; intros; auto with coc.
generalize H; elim (le_gt_dec k n); intros; auto with coc.
inversion_clear H0.

inversion_clear H1.
apply mem_abs_l; apply H with n k; auto with coc.

apply mem_abs_r; apply H0 with n (S k); auto with coc.

inversion_clear H1.
apply mem_app_l; apply H with n k; auto with coc.

apply mem_app_r; apply H0 with n k; auto with coc.

inversion_clear H1.
apply mem_prod_l; apply H with n k; auto with coc.

apply mem_prod_r; apply H0 with n (S k); auto with coc.
Qed.

  Lemma mem_sort_subst :
   ∀ b a n s,
   mem_sort s (subst_rec a b n) -> mem_sort s a \/ mem_sort s b.
simple induction b; simpl in |- *; intros; auto with coc.
generalize H; elim (lt_eq_lt_dec n0 n); intro.
elim a0; intros.
inversion_clear H0.

left.
apply mem_sort_lift with n0 0; auto with coc.

intros.
inversion_clear H0.

inversion_clear H1.
elim H with a n s; auto with coc.

elim H0 with a (S n) s; auto with coc.

inversion_clear H1.
elim H with a n s; auto with coc.

elim H0 with a n s; auto with coc.

inversion_clear H1.
elim H with a n s; auto with coc.

elim H0 with a (S n) s; intros; auto with coc.
Qed.

  Lemma exp_sort_mem : ∀ s t u, red1 t u -> mem_sort s u -> mem_sort s t.
induction 1; intros; try inversion_clear H0; auto.
apply mem_sort_subst in H; destruct H; auto.
Qed.

  Lemma red_sort_mem : ∀ t s, red t (Srt s) -> mem_sort s t.
intros.
pattern t in |- *.
apply red1_red_ind with (Srt s); auto with coc.
do 4 intro.
elim H0; intros.
elim mem_sort_subst with M0 N 0 s; intros; auto with coc.

inversion_clear H4; auto with coc.

inversion_clear H4; auto with coc.

inversion_clear H4; auto with coc.

inversion_clear H4; auto with coc.

inversion_clear H4; auto with coc.

inversion_clear H4; auto with coc.
Qed.

  Lemma red_normal : ∀ u v, red u v -> normal u -> u = v.
simple induction 1; auto with coc; intros.
absurd (red1 u N); auto with coc.
absurd (red1 P N); auto with coc.
elim (H1 H3).
unfold not in |- *; intro; apply (H3 N); auto with coc.
Qed.

  Lemma sn_red_sn : ∀ a b, sn a -> red a b -> sn b.
unfold sn in |- *.
simple induction 2; intros; auto with coc.
apply Acc_inv with P; auto with coc.
Qed.

  Lemma commut_red1_subterm : commut _ subterm (transp _ red1).
red in |- *.
simple induction 1; intros.
exists (Abs z B); auto with coc.

exists (Abs A z); auto with coc.

exists (App z B); auto with coc.

exists (App A z); auto with coc.

exists (Prod z B); auto with coc.

exists (Prod A z); auto with coc.
Qed.

  Lemma subterm_sn : ∀ a, sn a -> ∀ b, subterm b a -> sn b.
unfold sn in |- *.
simple induction 1; intros.
apply Acc_intro; intros.
elim commut_red1_subterm with x b y; intros; auto with coc.
apply H1 with x0; auto with coc.
Qed.

  Lemma sn_prod : ∀ A, sn A -> ∀ B, sn B -> sn (Prod A B).
unfold sn in |- *.
simple induction 1.
simple induction 3; intros.
apply Acc_intro; intros.
inversion_clear H5; auto with coc.
apply H1; auto with coc.
apply Acc_intro; auto with coc.
Qed.

  Lemma sn_subst : ∀ T M, sn (subst T M) -> sn M.
intros.
cut (∀ t, sn t -> ∀ m, t = subst T m -> sn m).
intros.
apply H0 with (subst T M); auto with coc.

unfold sn in |- *.
simple induction 1; intros.
apply Acc_intro; intros.
apply H2 with (subst T y); auto with coc.
rewrite H3.
unfold subst in |- *; auto with coc.
Qed.