fact: Fixpoint ren_poly_type (xi : nat -> nat) (s : poly_type) : poly_type := match s return poly_type with | poly_var x => poly_var (xi x) | poly_arr s t => poly_arr (ren_poly_type xi s) (ren_poly_type xi t) | poly_abs s => poly_abs (ren_poly_type (scons 0 (funcomp S xi)) s) end.
imports: List