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