proposition: Lemma eq_var_bool_refl : forall v, eq_var_bool v v = true.
proof: Proof. intro v. generalize (X.eq_bool_ok v v); case (eq_var_bool v v). intros _; reflexivity. intro v_diff_v; apply False_rect; apply v_diff_v; reflexivity. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)