+Instance KindEqDecidable : EqDecidable Kind.
+ apply Build_EqDecidable.
+ induction v1.
+ destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+ destruct v2; try (right; intro q; inversion q; fail) ; auto.
+ destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
+ right; intro; subst; inversion H; subst; apply n; auto.
+ destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+ destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+ destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+ destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+ Defined.
+