proposition: Lemma SPO_to_lex_SPO : forall (ss : list ES.A), (forall s, In s ss -> (forall t u, r s t -> r t u -> r s u) /\ (r s s -> False)) -> (forall ts us : list ES.A, lex ss ts -> lex ts us -> lex ss us) /\ (lex ss ss -> False).
proof: Proof. induction ss as [ | s ss IHss]; intro Hss; split. intros ts us Hss_ts Hts_us; inversion Hss_ts; subst; trivial. intro H; inversion H. intros ts us Hss_ts Hts_us. assert (Hs : In s (s::ss)). left; trivial. elim (Hss s Hs); intros Hss' Hss''. destruct ts as [ | t ts]; inversion Hss_ts; subst. destruct us as [ | u us]; inversion Hts_us; subst. constructor 1. apply Hss' with t; try left; trivial. rewrite H4; trivial. constructor 1; trivial. rewrite H4; apply lex_length; trivial. destruct us as [ | u us]; inversion Hts_us; subst. constructor 1; trivial. rewrite <- H5; apply lex_length; trivial. constructor 2. elim IHss. intros H2 H3; apply (H2 ts); trivial. intros s s_in_ss; split. elim (Hss s); try right; trivial. elim (Hss s); try right; trivial. intro H; inversion H; subst. elim (Hss s); try left; trivial; intros H1 H2. apply H2; hyp. elim IHss. intros H2 H3; apply H3; trivial. intros s' s'_in_ss; apply (Hss s'); try right; trivial. Qed.
imports: CoLoR(RelExtras ListUtil AccUtil LogicUtil)