# Library Termes

``` Require Export 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 : forall A B, subterm A (Abs A B)     | sbtrm_abs_r : forall A B, subterm B (Abs A B)     | sbtrm_app_l : forall A B, subterm A (App A B)     | sbtrm_app_r : forall A B, subterm B (App A B)     | sbtrm_prod_l : forall A B, subterm A (Prod A B)     | sbtrm_prod_r : forall A B, subterm B (Prod A B).   Inductive mem_sort (s : sort) : term -> Prop :=     | mem_eq : mem_sort s (Srt s)     | mem_prod_l : forall u v, mem_sort s u -> mem_sort s (Prod u v)     | mem_prod_r : forall u v, mem_sort s v -> mem_sort s (Prod u v)     | mem_abs_l : forall u v, mem_sort s u -> mem_sort s (Abs u v)     | mem_abs_r : forall u v, mem_sort s v -> mem_sort s (Abs u v)     | mem_app_l : forall u v, mem_sort s u -> mem_sort s (App u v)     | mem_app_r : forall u v, mem_sort s v -> mem_sort s (App u v). End Termes.   Hint Constructors subterm: coc.   Hint Constructors mem_sort: coc. Section Beta_Reduction.   Inductive red1 : term -> term -> Prop :=     | beta : forall M N T, red1 (App (Abs T M) N) (subst N M)     | abs_red_l :         forall M M', red1 M M' -> forall N, red1 (Abs M N) (Abs M' N)     | abs_red_r :         forall M M', red1 M M' -> forall N, red1 (Abs N M) (Abs N M')     | app_red_l :         forall M1 N1, red1 M1 N1 -> forall M2, red1 (App M1 M2) (App N1 M2)     | app_red_r :         forall M2 N2, red1 M2 N2 -> forall M1, red1 (App M1 M2) (App M1 N2)     | prod_red_l :         forall M1 N1, red1 M1 N1 -> forall M2, red1 (Prod M1 M2) (Prod N1 M2)     | prod_red_r :         forall M2 N2, red1 M2 N2 -> forall M1, red1 (Prod M1 M2) (Prod M1 N2).   Inductive red (M : term) : term -> Prop :=     | refl_red : red M M     | trans_red : forall 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 : forall P N, conv M P -> red1 P N -> conv M N     | trans_conv_exp : forall P N, conv M P -> red1 N P -> conv M N.   Inductive par_red1 : term -> term -> Prop :=     | par_beta :         forall 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 : forall s, par_red1 (Srt s) (Srt s)     | ref_par_red : forall n, par_red1 (Ref n) (Ref n)     | abs_par_red :         forall M M' T T',         par_red1 M M' -> par_red1 T T' -> par_red1 (Abs T M) (Abs T' M')     | app_par_red :         forall M M' N N',         par_red1 M M' -> par_red1 N N' -> par_red1 (App M N) (App M' N')     | prod_par_red :         forall 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 := forall u, ~ red1 t u.   Definition sn := Acc (transp _ red1). End Normalisation_Forte.   Hint Unfold sn: coc.   Lemma inv_lift_sort : forall 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 :     forall 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 :    forall 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 : forall 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 : forall 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 :    forall 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 : forall 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 : forall 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 : forall M, lift 0 M = M. intros; unfold lift in |- *. apply lift_rec0; auto with coc. Qed.   Lemma simpl_lift_rec :    forall 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 : forall 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 :    forall 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 :    forall 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 :    forall 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 :    forall 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 :    forall 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 :    forall 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 :    forall 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 :    forall 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 :    forall 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 :    forall 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 : forall 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 :    forall N P,    (P:term -> Prop) N ->    (forall M R, red1 M R -> red R N -> P R -> P M) ->    forall M, red M N -> P M. cut  (forall M N,   red M N ->   forall P : term -> Prop,   P N -> (forall 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 : forall 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 :    forall 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 :    forall 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 :    forall 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 :    forall n u v, red1 u v -> forall 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 :    forall a t u,    red1 t u -> forall 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 :    forall t u,    red1 t u -> forall 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 :    forall u v t,    red (Prod u v) t ->    forall P : Prop,    (forall 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 : forall 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 : forall M N, red1 M N -> conv N M. intros. apply trans_conv_exp with N; auto with coc. Qed.   Lemma red_conv : forall 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 : forall 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 : forall 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 :    forall 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 :    forall 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 :    forall 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 : forall M, par_red1 M M. simple induction M; auto with coc. Qed.   Hint Resolve refl_par_red1: coc.   Lemma red1_par_red1 : forall 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 : forall 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 : forall 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 :    forall n a b,    par_red1 a b -> forall 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 :    forall a b c d,    par_red1 a b ->    par_red1 c d -> forall 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 :    forall (P : Prop) T U x,    par_red1 (Abs T U) x ->    (forall 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 :    forall 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 :    forall 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 red_sort_mem : forall 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 : forall 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 : forall 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 : forall a, sn a -> forall 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 : forall A, sn A -> forall 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 : forall T M, sn (subst T M) -> sn M. intros. cut (forall t, sn t -> forall 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. ```