proposition: Lemma env_comp_ext_l : forall E1 E2, E1 [+] E2 [<->] E2.
proof: Proof. intros E1 E2 p A B E1E2_pA E2_pB. set (hint := env_sum_ry E1 E2_pB). inversion E1E2_pA. inversion hint. try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)