proposition: Lemma rinstInst_poly_type (xipoly_type : ( nat ) -> nat ) : ren_poly_type xipoly_type === subst_poly_type (funcomp (poly_var ) xipoly_type) .
proof: Proof. exact ((fun x => rinst_inst_poly_type xipoly_type (_) (fun n => eq_refl) x)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms