proposition: Lemma typ_sub_weak : forall g (d : term) t, typ g d t -> forall e u (U : term), typ e u U -> forall f n, sub_in_env d t n e f -> wf f -> trunc _ n f g -> typ f (subst_rec d u n) (subst_rec d U n).
proof: Proof. simple induction 2; simpl in |- *; intros; auto with coc core arith datatypes. elim (lt_eq_lt_dec n v); [ intro Hlt_eq | intro Hlt ]. elim H2. elim Hlt_eq; clear Hlt_eq. case v; [ intro Hlt | intros n0 Hlt ]; intros. inversion_clear Hlt. simpl in |- *. rewrite H6. rewrite simpl_subst; auto with coc core arith datatypes. apply type_var; auto with coc core arith datatypes. exists x; auto with coc core arith datatypes. apply nth_sub_sup with d t n e0; auto with coc core arith datatypes. intro Heq; intros. rewrite H6. elim Heq. rewrite simpl_subst; auto with coc core arith datatypes. replace x with t. apply thinning_n with g; auto with coc core arith datatypes. apply fun_item with e0 v; auto with coc core arith datatypes. apply nth_sub_eq with d f; auto with coc core arith datatypes. elim Heq; auto with coc core arith datatypes. apply type_var; auto with coc core arith datatypes. apply nth_sub_inf with t e0; auto with coc core arith datatypes. cut (wf (subst_rec d T n :: f)); intros. 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_subst. apply type_app with (subst_rec d V n); auto with coc core arith datatypes. cut (wf (subst_rec d T n :: f)); intros. 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 (subst_rec d U0 n) s; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList