proposition: Lemma trans_conv_conv : forall M N (P : term), conv M N -> conv N P -> conv M P.
proof: Proof. intros. generalize M H; elim H0; intros; auto with coc core arith sets. apply trans_conv_red with P0; auto with coc core arith sets. apply trans_conv_exp with P0; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations