fact: Fixpoint rinst_inst_term (xipoly_type : ( nat ) -> nat ) (xiterm : ( nat ) -> nat ) (sigmapoly_type : ( nat ) -> poly_type ) (sigmaterm : ( nat ) -> term ) (Eqpoly_type : forall x, (funcomp (poly_var ) xipoly_type) x = sigmapoly_type x) (Eqterm : forall x, (funcomp (var ) xiterm) x = sigmaterm x) (s : term ) : ren_term xipoly_type xiterm s = subst_term sigmapoly_type sigmaterm s := match s return ren_term xipoly_type xiterm s = subst_term sigmapoly_type sigmaterm s with | var s => Eqterm s | app s0 s1 => congr_app (rinst_inst_term xipoly_type xiterm sigmapoly_type sigmaterm Eqpoly_type Eqterm s0) (rinst_inst_term xipoly_type xiterm sigmapoly_type sigmaterm Eqpoly_type Eqterm s1) | abs s0 s1 => congr_abs (rinst_inst_poly_type xipoly_type sigmapoly_type Eqpoly_type s0) (rinst_inst_term (upRen_term_poly_type xipoly_type) (upRen_term_term xiterm) (up_term_poly_type sigmapoly_type) (up_term_term sigmaterm) (rinstInst_up_term_poly_type (_) (_) Eqpoly_type) (rinstInst_up_term_term (_) (_) Eqterm) s1) | ty_app s0 s1 => congr_ty_app (rinst_inst_term xipoly_type xiterm sigmapoly_type sigmaterm Eqpoly_type Eqterm s0) (rinst_inst_poly_type xipoly_type sigmapoly_type Eqpoly_type s1) | ty_abs s0 => congr_ty_abs (rinst_inst_term (upRen_poly_type_poly_type xipoly_type) (upRen_poly_type_term xiterm) (up_poly_type_poly_type sigmapoly_type) (up_poly_type_term sigmaterm) (rinstInst_up_poly_type_poly_type (_) (_) Eqpoly_type) (rinstInst_up_poly_type_term (_) (_) Eqterm) s0) end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms