fact: Fixpoint compSubstRen_term (sigmapoly_type : ( nat ) -> poly_type ) (sigmaterm : ( nat ) -> term ) (zetapoly_type : ( nat ) -> nat ) (zetaterm : ( nat ) -> nat ) (thetapoly_type : ( nat ) -> poly_type ) (thetaterm : ( nat ) -> term ) (Eqpoly_type : forall x, (funcomp (ren_poly_type zetapoly_type) sigmapoly_type) x = thetapoly_type x) (Eqterm : forall x, (funcomp (ren_term zetapoly_type zetaterm) sigmaterm) x = thetaterm x) (s : term ) : ren_term zetapoly_type zetaterm (subst_term sigmapoly_type sigmaterm s) = subst_term thetapoly_type thetaterm s := match s return ren_term zetapoly_type zetaterm (subst_term sigmapoly_type sigmaterm s) = subst_term thetapoly_type thetaterm s with | var s => Eqterm s | app s0 s1 => congr_app (compSubstRen_term sigmapoly_type sigmaterm zetapoly_type zetaterm thetapoly_type thetaterm Eqpoly_type Eqterm s0) (compSubstRen_term sigmapoly_type sigmaterm zetapoly_type zetaterm thetapoly_type thetaterm Eqpoly_type Eqterm s1) | abs s0 s1 => congr_abs (compSubstRen_poly_type sigmapoly_type zetapoly_type thetapoly_type Eqpoly_type s0) (compSubstRen_term (up_term_poly_type sigmapoly_type) (up_term_term sigmaterm) (upRen_term_poly_type zetapoly_type) (upRen_term_term zetaterm) (up_term_poly_type thetapoly_type) (up_term_term thetaterm) (up_subst_ren_term_poly_type (_) (_) (_) Eqpoly_type) (up_subst_ren_term_term (_) (_) (_) (_) Eqterm) s1) | ty_app s0 s1 => congr_ty_app (compSubstRen_term sigmapoly_type sigmaterm zetapoly_type zetaterm thetapoly_type thetaterm Eqpoly_type Eqterm s0) (compSubstRen_poly_type sigmapoly_type zetapoly_type thetapoly_type Eqpoly_type s1) | ty_abs s0 => congr_ty_abs (compSubstRen_term (up_poly_type_poly_type sigmapoly_type) (up_poly_type_term sigmaterm) (upRen_poly_type_poly_type zetapoly_type) (upRen_poly_type_term zetaterm) (up_poly_type_poly_type thetapoly_type) (up_poly_type_term thetaterm) (up_subst_ren_poly_type_poly_type (_) (_) (_) Eqpoly_type) (up_subst_ren_poly_type_term (_) (_) (_) (_) Eqterm) s0) end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms