proposition: Lemma env_subset_dropSuffix_eq : forall E, env_eq (dropEmptySuffix E) E.
proof: Proof. split; intros; intros p A D. apply dropSuffix_decl_rev; trivial. apply dropSuffix_decl; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)