proposition: Lemma eq_symb_bool_refl : forall f, eq_symb_bool f f = true.
proof: Proof. intro f. generalize (Symb.eq_bool_ok f f); case (eq_symb_bool f f). intros _; reflexivity. intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)