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