proposition: Lemma iter_up_poly_type_poly_type {n σ x} : Nat.iter n up_poly_type_poly_type σ (n + x) = ren_poly_type (Nat.add n) (σ x).
proof: Proof. elim: n x σ; first by move=> ? ?; rewrite ren_poly_type_id. move=> n IH x σ /=. by rewrite /funcomp IH poly_type_norm. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun