proposition: Lemma env_sum_length : forall El Er, length (El [+] Er) = Nat.max (length El) (length Er).
proof: Proof. induction El; intros. simpl; destruct Er; trivial. simpl; destruct Er; trivial. destruct o; simpl; rewrite IHEl; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)