proposition: Lemma typing_ext_env : forall Pt E E' A, envSubset E' E -> E' |- Pt := A -> E |- Pt := A.
proof: Proof. induction Pt. intros E E' A envC Ex. constructor. inversion Ex. apply envC; trivial. inversion 2; constructor. intros E E' a EE' TypAbs. inversion TypAbs. constructor. apply IHPt with (A [#] E'); trivial. apply env_subset_cons; trivial. intros E E' A EE' TypApp. inversion TypApp. constructor 4 with A0. apply IHPt1 with E'; trivial. apply IHPt2 with E'; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)