proposition: Lemma var_in_term_list_is_sound : forall x l, var_in_term_list x l = true <-> In x (var_list_list l).
proof: Proof. intros x l; functional induction (var_in_term_list x l) as [ | x' y l H1 IH | x' f ll l H1 IHll IHl]. simpl; intuition. simpl; rewrite <- IH. generalize (X.eq_bool_ok x y); case (eq_var_bool x y); simpl. intro x_eq_y; split. intros _; left; apply sym_eq; assumption. intros _; apply eq_refl. intro x_diff_y; split. intro x_in_l; right; assumption. intros [y_eq_x | x_in_l]; [apply False_rect; apply x_diff_y; apply sym_eq | idtac]; assumption. split; intro x_in_ll_l. destruct (Bool.orb_prop _ _ x_in_ll_l) as [x_in_ll | x_in_l]. apply in_or_app; left; rewrite <- IHll; assumption. apply in_or_app; right; rewrite <- IHl; assumption. case (in_app_or _ _ _ x_in_ll_l); [intro x_in_ll | intro x_in_l]. rewrite <- IHll in x_in_ll; rewrite x_in_ll; apply eq_refl. rewrite <- IHl in x_in_l; rewrite x_in_l; case (var_in_term_list x ll); apply eq_refl. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)