fact: Fixpoint compRenSubst_poly_type (xipoly_type : ( nat ) -> nat ) (taupoly_type : ( nat ) -> poly_type ) (thetapoly_type : ( nat ) -> poly_type ) (Eqpoly_type : forall x, (funcomp taupoly_type xipoly_type) x = thetapoly_type x) (s : poly_type ) : subst_poly_type taupoly_type (ren_poly_type xipoly_type s) = subst_poly_type thetapoly_type s := match s return subst_poly_type taupoly_type (ren_poly_type xipoly_type s) = subst_poly_type thetapoly_type s with | poly_var s => Eqpoly_type s | poly_arr s0 s1 => congr_poly_arr (compRenSubst_poly_type xipoly_type taupoly_type thetapoly_type Eqpoly_type s0) (compRenSubst_poly_type xipoly_type taupoly_type thetapoly_type Eqpoly_type s1) | poly_abs s0 => congr_poly_abs (compRenSubst_poly_type (upRen_poly_type_poly_type xipoly_type) (up_poly_type_poly_type taupoly_type) (up_poly_type_poly_type thetapoly_type) (up_ren_subst_poly_type_poly_type (_) (_) (_) Eqpoly_type) s0) end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms