fact: Fixpoint cases (i : itype ps) (k : asFunc ps Type -> asFunc ps Type) {struct i} : asFunc ps Type := match i with | Inj _ T => k (const T) | Sum a b => combine prod ps (cases a k) (cases b k) | Prod a b => cases a (fun A => cases b (fun B => under _ _ (fun App => App _ A -> App _ (k B)))) | Rec ps => k (const (applyF RecT (hlist_to_tuple ps))) | @Get _ T m f => @get _ _ _ m (fun x => cases (f x) k) | @Sig _ t f => @under _ _ (fun App => forall x' : t, (App _ (cases (f x') k))) | @Pi _ t f => @under _ _ (fun App => @sigT t (fun x' => App _ (cases (f x') k))) | @Unf _ T pf v i => replace pf v (cases i k) end.
imports: Coq.Lists.List ExtLib.Data.Member ExtLib.Data.HList ExtLib.Generic.Func