proposition: Lemma rinstInst_pure_term (xipure_term : ( nat ) -> nat ) : ren_pure_term xipure_term === subst_pure_term (funcomp (pure_var ) xipure_term) .
proof: Proof. exact ((fun x => rinst_inst_pure_term xipure_term (_) (fun n => eq_refl) x)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms