proposition: Lemma loweredEnv_distr_sum : forall El Er n, loweredEnv (El [+] Er) n = loweredEnv El n [+] loweredEnv Er n.
proof: Proof. intros. apply env_equiv_eq. apply loweredEnv_distr_sum_equiv. unfold loweredEnv. autorewrite with datatypes. rewrite !env_sum_length. autorewrite with datatypes. destruct (le_gt_dec (length El) (length Er)); lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)