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; inversion H. - right; intro H; inversion H. - destruct (IHx y); subst. + left; reflexivity. + right; intro H; depelim H. apply n0. contradiction. Qed.
imports: Program Equations.Prop.DepElim Equations.Prop.Equations Coq.Logic.Eqdep_dec Coq.Classes.EquivDec Arith