proposition: Lemma typ_conv_conv : forall e u (U : term) v (V : term), typ e u U -> typ e v V -> conv u v -> conv U V.
proof: Proof. intros. elim church_rosser with u v; auto with coc core arith datatypes; intros. apply typ_unique with e x. apply subject_reduction with u; auto with coc core arith datatypes. apply subject_reduction with v; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList