proposition: Theorem subject_reduction : forall e t u, red t u -> forall T, typ e t T -> typ e u T.
proof: Proof. simple induction 1; intros; auto with coc core arith datatypes. apply subj_red with P; intros; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList