proposition: Lemma bprec_eq_status_ok : bprec_eq_status Fs = true -> forall f g, prec_eq prec_nat f g -> status f = status g.
proof: Proof. intros. eapply bprec_eq_status_aux2_ok. ehyp. apply Fs_ok. apply Fs_ok. 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)