proposition: Lemma bprec_eq_status_aux2_ok : forall fs b, bprec_eq_status_aux2 b fs = true -> forall f g, In f fs -> In g fs -> prec_eq prec_nat f g -> status f = status g.
proof: Proof. induction fs; simpl; intros. contr. destruct H0; destruct H1. subst f. subst g. refl. subst f. ded (bprec_eq_status_aux2_true H). apply (bprec_eq_status_aux1_ok H0); hyp. subst g. ded (bprec_eq_status_aux2_true H). sym. apply (bprec_eq_status_aux1_ok H1). hyp. apply prec_eq_sym. hyp. eapply IHfs; ehyp. 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)