proposition: Lemma map_ren_poly_type_id {Gamma} : map (ren_poly_type id) Gamma = Gamma.
proof: Proof. under map_ext => ? do rewrite ren_poly_type_id. by rewrite map_id. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun