- Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind )(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
- gaTy TV ec (ga_mk_tree' ec ant) (ga_mk_tree' ec suc).
+ Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
+ gaTy TV ec
+ (ga_mk_tree' ec (ant,,(mapOptionTreeAndFlatten (unleaves ○ take_arg_types) suc)))
+ (ga_mk_tree' ec ( mapOptionTree drop_arg_types suc) ).