proposition: Lemma wf_sort_lift : forall n e t, wf e -> item_lift t e n -> exists s : sort, typ e t (Srt s).
proof: Proof. simple induction n. simple destruct e; intros. elim H0; intros. inversion_clear H2. elim H0; intros. rewrite H1. inversion_clear H2. inversion_clear H. exists s. replace (Srt s) with (lift 1 (Srt s)); auto with coc core arith datatypes. apply thinning; auto with coc core arith datatypes. apply wf_var with s; auto with coc core arith datatypes. intros. elim H1; intros. rewrite H2. generalize H0. inversion_clear H3; intros. rewrite simpl_lift; auto with coc core arith datatypes. cut (wf l); intros. elim H with l (lift (S n0) x); intros; auto with coc core arith datatypes. inversion_clear H3. exists x0. change (typ (y :: l) (lift 1 (lift (S n0) x)) (lift 1 (Srt x0))) in |- *. apply thinning; auto with coc core arith datatypes. apply wf_var with s; auto with coc core arith datatypes. exists x; auto with coc core arith datatypes. inversion_clear H3. apply typ_wf with y (Srt s); auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList