fact: Fixpoint expand_fun' (l : list Type) : forall T U : Type, expand_type l T -> (T -> U) -> expand_type l U := match l as l return forall T U, expand_type l T -> (T ->U) -> expand_type l U with | nil => fun T U f a => a f | cons T' l => fun T U f a => expand_fun' l (T' -> T) (T' -> U) f (fun g xn => a (g xn)) end.
imports: ZArith