fact: Fixpoint asPi_combine ps {struct ps} : forall (F G : _), asPi ps (fun App => F App -> G App) -> asPi ps F -> asPi ps G := match ps as ps return forall F G : (forall U : Type, asFunc ps U -> U) -> Type, asPi ps (fun App : forall U : Type, asFunc ps U -> U => F App -> G App) -> asPi ps F -> asPi ps G with | nil => fun _ _ a b => a b | p :: ps => fun _ _ a b x => asPi_combine _ _ _ (a x) (b x) end.
imports: Coq.Lists.List ExtLib.Data.Member ExtLib.Data.HList ExtLib.Generic.Func