proposition: Lemma thinning_n : forall n e f, trunc _ n e f -> forall t T, typ f t T -> wf e -> typ e (lift n t) (lift n T).
proof: Proof. simple induction n. intros. rewrite lift0. rewrite lift0. replace e with f; auto with coc core arith datatypes. inversion_clear H; auto with coc core arith datatypes. do 8 intro. inversion_clear H0. intro. rewrite simpl_lift; auto with coc core arith datatypes. pattern (lift (S n0) T) in |- *. rewrite simpl_lift; auto with coc core arith datatypes. inversion_clear H0. change (typ (x :: e0) (lift 1 (lift n0 t)) (lift 1 (lift n0 T))) in |- *. apply thinning; auto with coc core arith datatypes. apply H with f; auto with coc core arith datatypes. apply typ_wf with x (Srt s); auto with coc core arith datatypes. apply wf_var with s; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList