proposition: Lemma rinstInst_term (xipoly_type : ( nat ) -> nat ) (xiterm : ( nat ) -> nat ) : ren_term xipoly_type xiterm === subst_term (funcomp (poly_var ) xipoly_type) (funcomp (var ) xiterm) .
proof: Proof. exact ((fun x => rinst_inst_term xipoly_type xiterm (_) (_) (fun n => eq_refl) (fun n => eq_refl) x)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms