proposition: Lemma lex_lifting : forall (r : relation ES.A) (l : list ES.A), Accs r l -> Restricted_acc (Accs r) (lex r) l.
proof: Proof. intros r l; apply (lex_lifting_aux r (length l) l); trivial. Qed.
imports: CoLoR(RelExtras ListUtil AccUtil LogicUtil)