proposition: Lemma equiv_same_top : forall f g l l', equiv (Term f l) (Term g l') -> prec_eq Prec f g.
proof: Proof. intros f g l l' H; inversion H; subst; trivial. apply prec_eq_refl. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)