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).