proposition: Lemma irrefl_to_lex_irrefl : forall (ss : list ES.A), (forall s, In s ss -> r s s -> False) -> lex ss ss -> False.
proof: Proof. intro ss; induction ss as [ | h ss IHss]; intros Hss Hlex; inversion Hlex; subst. apply Hss with h; try left; trivial. apply IHss; trivial. intros s s_in_ss; apply Hss; try right; trivial. Qed.
imports: CoLoR(RelExtras ListUtil AccUtil LogicUtil)