proposition: Lemma ren_poly_type_allfv_id {ξ t} : (allfv_poly_type (fun x => ξ x = x) t) -> ren_poly_type ξ t = t.
proof: Proof. rewrite -[RHS]ren_poly_type_id => ?. by apply: ext_ren_poly_type_allfv_poly_type. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun