proposition: Lemma env_comp_sum_l : forall M N, M [<->] N [+] M.
proof: Proof. intros. intros p A B Mp NMp. set (w := env_sum_ry N Mp). inversion NMp; inversion w; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)