+let pack asts =
+ List.fold_right
+ (fun ast acc -> Binder (`Forall, (Cic.Anonymous, Some ast), acc))
+ asts (Sort `Type)
+
+let rec unpack = function
+ | Binder (`Forall, (Cic.Anonymous, Some ast), Sort `Type) -> [ast]
+ | Binder (`Forall, (Cic.Anonymous, Some ast), tgt) -> ast :: unpack tgt
+ | _ -> assert false
+