fact: Fixpoint subst_term (sigmapoly_type : ( nat ) -> poly_type ) (sigmaterm : ( nat ) -> term ) (s : term ) : term := match s return term with | var s => sigmaterm s | app s0 s1 => app (subst_term sigmapoly_type sigmaterm s0) (subst_term sigmapoly_type sigmaterm s1) | abs s0 s1 => abs (subst_poly_type sigmapoly_type s0) (subst_term (up_term_poly_type sigmapoly_type) (up_term_term sigmaterm) s1) | ty_app s0 s1 => ty_app (subst_term sigmapoly_type sigmaterm s0) (subst_poly_type sigmapoly_type s1) | ty_abs s0 => ty_abs (subst_term (up_poly_type_poly_type sigmapoly_type) (up_poly_type_term sigmaterm) s0) end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms