proposition: Lemma env_comp_sum_comp_right : forall E1 E2 E3, E1 [<->] E2 [+] E3 -> E1 [<->] E3.
proof: Proof. intros E1 E2 E3 E1_23 p A B E1_pA E3_pB. exact (E1_23 p A B E1_pA (env_sum_ry E2 E3_pB)). Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)