proposition: Lemma isVarDecl_dec : forall E x, {A: SimpleType | E |= x := A} + {E |= x :!}.
proof: Proof. intros; unfold VarUD. destruct (nth_error_In E x) as [[A ExA] | Exn]. destruct A. left; exists s; trivial. right; auto. right; auto. Defined.
imports: Coq(Eqdep_dec) CoLoR(RelExtras ListExtras LogicUtil)