proposition: Lemma var_in_term_is_sound : forall x t, var_in_term x t = true <-> In x (var_list t).
proof: Proof. intros x t; case t; clear t. intro y; simpl; split; generalize (X.eq_bool_ok y x); case (eq_var_bool y x). intros y_eq_x _; left; assumption. intros _ Abs; discriminate. intros _ _; reflexivity. intros y_diff_x y_in_x; case y_in_x; clear y_in_x. intro y_eq_x; absurd (y = x); assumption. intro Abs; elim Abs. intros f l; simpl. apply var_in_term_list_is_sound. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)