proposition: Lemma var_dec_eq : forall {n} (x y : var n), {x = y} + {x <> y}.
proof: Proof. depind x; depelim y. - left; reflexivity. - right; intro H; depelim H. - right; intro H; depelim H. - destruct (IHx y); subst. + left; reflexivity. + right; intro H; depelim H. contradiction. Qed.
imports: Program Equations(Equations) Coq.Classes.EquivDec Arith