proposition: Lemma bprec_eq_status_aux1_ok : forall gs b, bprec_eq_status_aux1 b gs = true -> forall g, In g gs -> prec_eq prec_nat f g -> status f = status g.
proof: Proof. induction gs; simpl; intros. contr. destruct H0. subst g. ded (bprec_eq_status_aux1_true H). rewrite andb_eq in H0. destruct H0. rewrite bprec_eq_status_symb_ok in H2. intuition. eapply IHgs. apply H. hyp. 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)