Axiom coreVar_eq_refl : forall v, (coreVar_eq v v) = (left _ (refl_equal v)).
Instance CoreVarEqDecidable : EqDecidable CoreVar :=
{ eqd_dec := coreVar_eq
Axiom coreVar_eq_refl : forall v, (coreVar_eq v v) = (left _ (refl_equal v)).
Instance CoreVarEqDecidable : EqDecidable CoreVar :=
{ eqd_dec := coreVar_eq