proposition: Lemma env_subset_comp : forall E E', envSubset E E' -> E [<->] E'.
proof: Proof. intros; intros x A B D1 D2. set (w := H x A D1). inversion D2; inversion w; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)