proposition: Lemma is_def_equiv : forall f : symbol, is_def f = true <-> defined rules f.
proof: Proof. intros f. unfold is_def. rewrite <- defined_list_equiv. rewrite (inb_equiv _ F.Symb.eq_bool) . reflexivity. clear;intros f g. generalize (F.Symb.eq_bool_ok f g). case (F.Symb.eq_bool f g);[tauto|intuition discriminate]. Qed.
imports: Coq(List Bool FunInd) CoLoR(weaved_relation closure term_spec terminaison)