proposition: Lemma eq_elem_to_eq_list_dec : forall ss : terms, (forall s, In s ss -> forall t, s = t \/ s <> t) -> forall ts, ss = ts \/ ss <> ts.
proof: Proof. intro ss; induction ss as [ | s ss IHss]; intros Hss ts. destruct ts; [left; trivial | right; intro H; inversion H]. destruct ts as [ | t ts]; [right; intro H; inversion H | idtac]. assert (H : In s (s :: ss)). left; trivial. elim (Hss s H t); intro case_s_t. subst t. assert (H' : forall s, In s ss -> forall t, s = t \/ s <> t). intros s' s'_in_ss; apply Hss; try right; trivial. gen (IHss H'); clear IHss; intro IHss. elim (IHss ts); intro case_ts. subst ss; left; trivial. right; injection; trivial. right; injection; trivial. Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)