proposition: Fact map_subst_poly_type_poly_var {Gamma} : map (subst_poly_type poly_var) Gamma = Gamma.
proof: Proof. rewrite (map_ext _ id); [|apply: map_id]. move => ?. by rewrite subst_poly_type_poly_var. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun