proposition: Theorem eq_var_dec: forall x y : NVar, {x = y} + {x <> y}.
proof: Proof. intros. remember (beq_var x y) as b. destruct b. left. apply beq_var_eq. auto. right. apply beq_var_false_not_eq. auto. Defined.
imports: list Omega