fact: Fixpoint under (domain : list Type) (range : Type) {struct domain} : ((forall U, asFunc domain U -> U) -> range) -> asFunc domain range := match domain as domain return ((forall U, asFunc domain U -> U) -> range) -> asFunc domain range with | nil => fun F => F (fun _ x => x) | d :: ds => fun F x => under ds range (fun App => F (fun U f => App U (f x))) end%type.
imports: Coq.Lists.List ExtLib.Data.Member