proposition: Lemma typ_weak_weak : forall A e t T, typ e t T -> forall n f, ins_in_env A n e f -> wf f -> typ f (lift_rec 1 t n) (lift_rec 1 T n).
proof: Proof. simple induction 1; simpl in |- *; intros; auto with coc core arith datatypes. elim (le_gt_dec n v); intros; apply type_var; auto with coc core arith datatypes. elim H1; intros. exists x. rewrite H4. unfold lift in |- *. rewrite simpl_lift_rec; simpl in |- *; auto with coc core arith datatypes. apply ins_item_ge with A n e0; auto with coc core arith datatypes. apply ins_item_lt with A e0; auto with coc core arith datatypes. cut (wf (lift_rec 1 T0 n :: f)). intro. apply type_abs with s1 s2; auto with coc core arith datatypes. apply wf_var with s1; auto with coc core arith datatypes. rewrite distr_lift_subst. apply type_app with (lift_rec 1 V n); auto with coc core arith datatypes. cut (wf (lift_rec 1 T0 n :: f)). intro. apply type_prod with s1; auto with coc core arith datatypes. apply wf_var with s1; auto with coc core arith datatypes. apply type_conv with (lift_rec 1 U n) s; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList