fact: Fixpoint ren_pure_term (xipure_term : ( nat ) -> nat ) (s : pure_term ) : pure_term := match s return pure_term with | pure_var s => (pure_var ) (xipure_term s) | pure_app s0 s1 => pure_app (ren_pure_term xipure_term s0) (ren_pure_term xipure_term s1) | pure_abs s0 => pure_abs (ren_pure_term (upRen_pure_term_pure_term xipure_term) s0) end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms