proposition: Lemma trans_Econv_Econv : forall M N P : term, Econv M N -> Econv N P -> Econv M P.
proof: Proof. intros. generalize M H; elim H0; intros; auto with ecoc coc core arith sets. apply Etrans_conv_red with P0; auto with ecoc coc core arith sets. apply Etrans_conv_exp with P0; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv