proposition: Lemma iter_up_poly_type_poly_type_ge {n σ x} : x >= n -> Nat.iter n up_poly_type_poly_type σ x = ren_poly_type (Nat.add n) (σ (x - n)).
proof: Proof. move=> ?. have {1}->: x = n + (x - n) by lia. by rewrite iter_up_poly_type_poly_type. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun