proposition: Lemma typ_red_env : forall e t T, typ e t T -> forall f, red1_in_env e f -> wf f -> typ f t T.
proof: Proof. simple induction 1; intros. auto with coc core arith datatypes. auto with coc core arith datatypes. elim red_item with v t0 e0 f; auto with coc core arith datatypes; intros. inversion_clear H4. inversion_clear H6. elim H1; intros. elim item_trunc with term v e0 x0; intros; auto with coc core arith datatypes. elim wf_sort with v e0 x1 x0; auto with coc core arith datatypes. intros. apply type_conv with x x2; auto with coc core arith datatypes. rewrite H6. replace (Srt x2) with (lift (S v) (Srt x2)); auto with coc core arith datatypes. apply thinning_n with x1; auto with coc core arith datatypes. cut (wf (T0 :: 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. apply type_app with V; auto with coc core arith datatypes. cut (wf (T0 :: 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 U s; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList