proposition: Lemma instId_poly_type : subst_poly_type (poly_var ) === id .
proof: Proof. exact ((fun x => idSubst_poly_type (poly_var ) (fun n => eq_refl) (id x))). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms