proposition: Lemma iter_up_poly_type_poly_type_lt {n σ x} : x < n -> Nat.iter n up_poly_type_poly_type σ x = poly_var x.
proof: Proof. elim: n x σ; first by lia. move=> n IH [|x] σ /= ?; first done. by rewrite /funcomp IH; first by lia. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun