proposition: Lemma bprec_eq_status_aux1_true : forall gs b, bprec_eq_status_aux1 b gs = true -> b = true.
proof: Proof. induction gs; simpl; intros. hyp. cut (b && bprec_eq_status_symb f a = true). rewrite andb_eq. intuition. apply IHgs. 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)