proposition: Lemma subj_red : forall e t T, typ e t T -> forall u, red1 t u -> typ e u T.
proof: Proof. simple induction 1; intros. inversion_clear H1. inversion_clear H1. inversion_clear H2. inversion_clear H6. cut (wf (M' :: e0)); intros. apply type_conv with (Prod M' U) s2; auto with coc core arith datatypes. apply type_abs with s1 s2; auto with coc core arith datatypes. apply typ_red_env with (T0 :: e0); auto with coc core arith datatypes. apply typ_red_env with (T0 :: e0); auto with coc core arith datatypes. apply type_prod with s1; auto with coc core arith datatypes. apply wf_var with s1; auto with coc core arith datatypes. apply type_abs with s1 s2; auto with coc core arith datatypes. elim type_case with e0 u (Prod V Ur); intros; auto with coc core arith datatypes. inversion_clear H5. apply inv_typ_prod with e0 V Ur (Srt x); intros; auto with coc core arith datatypes. generalize H2 H3. clear H2 H3. inversion_clear H4; intros. apply inv_typ_abs with e0 T0 M (Prod V Ur); intros; auto with coc core arith datatypes. apply type_conv with (subst v T1) s2; auto with coc core arith datatypes. apply substitution with T0; auto with coc core arith datatypes. apply type_conv with V s0; auto with coc core arith datatypes. apply inv_conv_prod_l with Ur T1; auto with coc core arith datatypes. unfold subst in |- *. apply conv_conv_subst; auto with coc core arith datatypes. apply inv_conv_prod_r with T0 V; auto with coc core arith datatypes. replace (Srt s2) with (subst v (Srt s2)); auto with coc core arith datatypes. apply substitution with V; auto with coc core arith datatypes. apply type_app with V; auto with coc core arith datatypes. apply type_conv with (subst N2 Ur) s2; auto with coc core arith datatypes. apply type_app with V; auto with coc core arith datatypes. unfold subst in |- *. apply conv_conv_subst; auto with coc core arith datatypes. replace (Srt s2) with (subst v (Srt s2)); auto with coc core arith datatypes. apply substitution with V; auto with coc core arith datatypes. discriminate H5. inversion_clear H4. apply type_prod with s1; auto with coc core arith datatypes. apply typ_red_env with (T0 :: e0); auto with coc core arith datatypes. apply wf_var with s1; auto with coc core arith datatypes. apply type_prod 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