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