proposition: Lemma prec_eq_ok : forall f g, prec_eq_bool prec_nat f g = true <-> prec_eq prec_nat f g.
proof: Proof. intros f g. gen (prec_eq_bool_ok prec_nat f g). intuition. rewrite H1 in H. hyp. case_eq (prec_eq_bool prec_nat f g); intros. refl. rewrite H2 in H. absurd (prec_eq prec_nat f g); hyp. Qed.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil) CoLoR(NatUtil) Coq(List Relations) CoLoR(term SN ASubstitution) CoLoR(rpo rpo_extension) CoLoR(ARedPair ARelation RelUtil BoolUtil)