proposition: Lemma env_comp_dropSuffix : forall E1 E2, E1 [<->] dropEmptySuffix E2 -> E1 [<->] E2.
proof: Proof. intros; intros p A B Dl Dr. apply (H p); trivial. apply dropSuffix_decl; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)