proposition: Lemma typing_ext_env_r : forall Pt E E' A, E [<->] E' -> E |- Pt := A -> E [+] E' |- Pt := A.
proof: Proof. induction Pt. intros E E' A envC Ex. constructor. inversion Ex. apply env_sum_ly; trivial. inversion 2; constructor. intros E E' a EE' TypAbs. inversion TypAbs. constructor. change (decl A (E [+] E')) with (decl A E [+] decl A E'). apply IHPt; trivial. unfold decl; apply env_comp_cons; auto. intros E E' A EE' 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)