proposition: Lemma typing_ext_env_l : forall Pt E E' A, E |- Pt := A -> E' [+] E |- Pt := A.
proof: Proof. induction Pt. intros E E' A Ex. constructor. inversion Ex. apply env_sum_ry; trivial. inversion 1; constructor. intros E E' a TypAbs. inversion TypAbs. constructor. change (decl A (E'[+]E)) with (decl A E' [+] decl A E). apply IHPt; trivial. intros E E' A TypApp. inversion TypApp. constructor 4 with A0. apply IHPt1; trivial. apply IHPt2; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)