proposition: Lemma iter_up_ren {n ξ x} : Nat.iter n up_ren ξ (n + x) = n + ξ x.
proof: Proof. elim: n x ξ; first done. move=> n IH x ξ /=. rewrite /funcomp IH. by lia. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun