Library STLC_Dec_Soundness
Require Import Metatheory
STLC_Dec_Definitions
STLC_Dec_Infrastructure.
Typing is preserved by weakening.
Lemma typing_weaken : forall G E F t T,
(E & G) |= t ~: T ->
ok (E & F & G) ->
(E & F & G) |= t ~: T.
Typing is preserved by substitution.
Lemma typing_subst : forall F U E t T z u,
(E & z ~ U & F) |= t ~: T ->
E |= u ~: U ->
(E & F) |= [z ~> u]t ~: T.
Preservation (typing is preserved by reduction).
Lemma preservation_result : preservation.
Progress (a well-typed term is either a value or it can
take a step of reduction).
Lemma progress_result : progress.