fact: Definition dataList (a : Type) : @data unit (fun _ => list a) := @Sigma _ _ bool (fun x => match x with | true => @Inj _ _ unit | false => @Prod _ _ (Inj _ a) (Get _ tt) end).
imports: String List ExtLib.Data.HList