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