proposition: Lemma beq_status_ok : forall s1 s2, beq_status s1 s2 = true <-> s1 = s2.
proof: Proof. beq_symb_ok. 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)