proposition: Lemma symb_list_ok : forall f t, In f (symb_list t) <-> symb_in_term f t = true.
proof: Proof. intros f t; pattern t; apply term_rec3; clear t. intros v; simpl; split; intro H; [contradiction H | discriminate H]. intros g l IH; simpl. generalize (F.Symb.eq_bool_ok f g); destruct (eq_symb_bool f g); [intro f_eq_g | intro f_diff_g]; simpl. split; [intros _; apply eq_refl | intros _; left; apply sym_eq; assumption]. split; [intros [H | H] | intro H]. apply False_rect; apply f_diff_g; apply sym_eq; assumption. induction l as [ | t l]. contradiction H. destruct (in_app_or _ _ _ H) as [f_in_t | f_in_l]. rewrite (IH _ (or_introl _ (eq_refl _))) in f_in_t; rewrite f_in_t; apply eq_refl. rewrite IHl. destruct (symb_in_term f t); apply eq_refl. intros; apply IH; right; assumption. assumption. right. induction l as [ | t l]. discriminate H. case_eq (symb_in_term f t); [intro f_in_t | intro f_not_in_t]. apply in_or_app; left; rewrite IH; [assumption | left; apply eq_refl]. apply in_or_app; right; apply IHl. intros; apply IH; right; assumption. rewrite f_not_in_t in H; assumption. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)