Library STLC_Dec_Decidability

Require Import Decidable Metatheory
  STLC_Dec_Definitions
  STLC_Dec_Infrastructure
  STLC_Dec_Soundness.

Equality on types is decidable

Lemma eq_typ_dec : forall (T T' : typ),
  sumbool (T = T') (T <> T').

Existence of a binding in the environment is decidable

Lemma binds_typ_dec : forall x (T : typ) E,
  decidable (binds x T E).

Renaming lemma for the typing relation

Lemma typing_rename : forall x y E t T U,
  x \notin (fv t \u dom E) ->
  y \notin (fv t \u dom E) ->
  (E & x ~ U) |= (t ^ x) ~: T ->
  (E & y ~ U) |= (t ^ y) ~: T.

Typing is decidable

Lemma typing_dec' : forall t E T, term t -> ok E ->
  decidable (E |= t ~: T).