Library STLC_Core_WF_Soundness
Require Import Metatheory
STLC_Core_WF_Definitions
STLC_Core_WF_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 E t T z u 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.