Trouble with heterogeneous equality

gistfile1.coq

Set Implicit Arguments.

Require Import Arith.Arith_base List Omega.
Require Import Wellfounded.Lexicographic_Product.
Require Import Relation_Operators.
Require Import JMeq.

(* Notation for heterogeneous equality *)

Infix "==" := JMeq (at level 70, no associativity).

(* kind definitions *)

Inductive Kind : Set :=
  | Star : Kind
  | KFun : Kind -> Kind -> Kind.

Notation "*" := Star.
Notation "k '==>' k'" := (KFun k k') (at level 60, right associativity).

Definition VarCtx := list Kind.
Definition ConCtx := list Kind.

(* type definition *)

Inductive Ty (C : ConCtx) (V : VarCtx) : Kind -> Set :=
  | var : forall k, In k V -> Ty C V k
  | con : forall k, In k C -> Ty C V k
  | app : forall k k', Ty C V (k ==> k') -> Ty C V k -> Ty C V k'.

Definition eq_ty_dec : forall {C V k}(t t' : Ty C V k), {t == t'} + {~ (t == t')}.
   intros C V k t ;
   induction t ; intro t' ; destruct t' ;
   try repeat (match goal with
                 | [V : VarCtx |- context[var _ _ _ _ == var _ _ _ _]] => left
                 | [|- context[con _ _ _ _ == con _ _ _ _]] => left 
                 | [|- context[app _ _ == app _ _]] => left
                 | [|- _ ] => let x := fresh "H" in right ; intro x
               end).

Wow... This is really a much better solution! Thanks for your time, Jason!