proposition: Lemma prec_transitive : transitive prec.
proof: Proof. intros s1 s2 s3; destruct s1; destruct s2; destruct s3; simpl; intros; trivial; contradiction. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)