proposition: Lemma Incomp23 : forall f, defined R2 f -> defined R3 f -> False.
proof: Proof. intros f D2 D3; inversion D2 as [h' l2 u2 H2]; clear D2; subst. assert (H := Indep3 u2 (Term f l2) f D3 H2). simpl in H; destruct (symb_in_term f u2). discriminate. revert H; simpl; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _; discriminate | intros f_diff_f; absurd (f=f); trivial]. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)