proposition: Lemma constructor_defined_dec : forall R rule_list, (forall l r, R r l <-> In (l,r) rule_list) -> forall f, {constructor R f} + {defined R f}.
proof: Proof. intros R rule_list H f. destruct (defined_dec R rule_list H f). right;assumption. left. constructor. intros;intro abs;apply n. apply (Def R f l t abs). Defined.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)