proposition: Lemma iter_up_ren_ge' {ξ n n' x}: x >= n -> Nat.iter (n + n') up_ren ξ x = n + Nat.iter n' up_ren ξ (x - n).
proof: Proof. move=> ?. have [?|?] : x < n + n' \/ n + n' <= x by lia. - rewrite ?iter_up_ren_lt; by lia. - have ? : ξ (x - (n + n')) = ξ (x - n - n') by congr ξ; lia. by rewrite ?iter_up_ren_ge; lia. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun