Prove that subject expansion does not hold for Stlc in Lemma not_subject_expansion
Prove soundness corollary in StlcProp
Prove type_uniqueness theorem in StlcProp