fact: Fixpoint extRen_poly_type (xipoly_type : ( nat ) -> nat ) (zetapoly_type : ( nat ) -> nat ) (Eqpoly_type : forall x, xipoly_type x = zetapoly_type x) (s : poly_type ) : ren_poly_type xipoly_type s = ren_poly_type zetapoly_type s := match s return ren_poly_type xipoly_type s = ren_poly_type zetapoly_type s with | poly_var s => ap (poly_var ) (Eqpoly_type s) | poly_arr s0 s1 => congr_poly_arr (extRen_poly_type xipoly_type zetapoly_type Eqpoly_type s0) (extRen_poly_type xipoly_type zetapoly_type Eqpoly_type s1) | poly_abs s0 => congr_poly_abs (extRen_poly_type (upRen_poly_type_poly_type xipoly_type) (upRen_poly_type_poly_type zetapoly_type) (upExtRen_poly_type_poly_type (_) (_) Eqpoly_type) s0) end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms