proposition: Lemma bprec_eq_status_symb_ok : forall f g, bprec_eq_status_symb f g = true <-> (prec_eq prec_nat f g -> status f = status g).
proof: Proof. intros f g. unfold bprec_eq_status_symb, implb. case_eq (prec_eq_bool prec_nat f g); intros. rewrite prec_eq_ok in H. rewrite beq_status_ok. intuition. intuition. rewrite <- prec_eq_ok, H in H1. discr. 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)