proposition: Lemma VarD_unique : forall E x A (v1 v2 : VarD E x A), v1 = v2.
proof: Proof. unfold VarD; intros; generalize v1 v2; rewrite v1. intros; apply K_dec_type; [idtac | pattern v0; apply K_dec_type]; auto; decide equality; generalize a o; decide equality; apply eq_SimpleType_dec. Qed.
imports: Coq(Eqdep_dec) CoLoR(RelExtras ListExtras LogicUtil)