proposition: Lemma type_reduction : forall e t T (U : term), red T U -> typ e t T -> typ e t U.
proof: Proof. intros. elim type_case with e t T; intros; auto with coc core arith datatypes. inversion_clear H1. apply type_conv with T x; auto with coc core arith datatypes. apply subject_reduction with T; auto with coc core arith datatypes. elim red_normal with T U; auto with coc core arith datatypes. rewrite H1. red in |- *; red in |- *; intros. inversion_clear H2. Qed.
imports: Termes Conv MyList