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