proposition: Lemma prelift_prelower : forall M M0, term (lift (lower M M0) 1) = term M.
proof: Proof. intros. autorewrite with terms; unfold prelift, prelower. rewrite (prelift_prelower_aux M M0); trivial. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)