proposition: Lemma clash : forall f g l1 l2, f<> g -> unit_theory f = Nothing -> unit_theory g = Nothing -> acu (Term f l1) (Term g l2) -> False.
proof: Proof. intros f g l1 l2 f_diff_g UTf UTg H; apply f_diff_g. generalize (acu_is_ac_on_unit_nf (Term f l1) (Term g l2)); intros [_ H']. generalize (H' H); clear H' H; intro H; simpl in H; rewrite UTf in H; rewrite UTg in H. generalize (ac_top_eq H); destruct l1 as [ | s1 [ | t1 [ | u1 l1]]]; destruct l2 as [ | s2 [ | t2 [ | u2 l2]]]; trivial. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)