proposition: Lemma Incomp13 : forall f, defined R1 f -> defined R3 f -> False.
proof: Proof. inversion module_R1_R3 as [M3]. intros f D1 D3; inversion D1 as [h' l1 u1 H1]; clear D1; subst. assert (H := M3 f u1 (Term f l1) D3 H1). simpl in H; destruct (symb_in_term f u1). 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)