proposition: Lemma Incomp : forall (R : relation term), is_primary_pi pi R -> ~defined R pi.
proof: Proof. intros R P D; inversion D as [f l u H]; subst f. destruct (P u (Term pi l) H pi) as [_ F]. apply F; trivial. revert F; simpl; generalize (F.Symb.eq_bool_ok pi pi); case (F.Symb.eq_bool pi pi); [intros _ | intros pi_diff_pi; absurd (pi = pi)]; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)