proposition: Lemma typing_drop_suffix : forall E Pt A, E |- Pt := A -> dropEmptySuffix E |- Pt := A.
proof: Proof. intros. apply typing_ext_env with E; trivial. apply (proj2 (env_subset_dropSuffix_eq E)). Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)