proposition: Lemma bsucceq_ok : forall t u, bsucceq t u = true -> succeq t u.
proof: Proof. intros t u. unfold bsucceq. gen (rpo_eval_is_sound (term_of_aterm t) (term_of_aterm u)). case (rpo_eval (term_of_aterm t) (term_of_aterm u)); try discr. destruct c; try discr; unfold succeq, Relation_Operators.union, equiv_aterm, succ, transp, Rof; auto. 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)