proposition: Lemma prelift_fold : forall Pt m n, prelift Pt (m + n) = prelift (prelift Pt n) m.
proof: Proof. intros Pt m n. unfold prelift. apply prelift_aux_fold. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)