proposition: Lemma lower_term : forall M ME, term (lower M ME) = prelower (term M).
proof: Proof. intros; unfold lower. destruct (lower_aux M ME); try_solve. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)