fix: use prop wherever possible

Author: TWal

src/Comparse.Parser.Builtins.fsti

@@ -137,7 +137,7 @@ let prefixes_length (#bytes:Type) {|bytes_like bytes|} (l:list bytes) =
 ///       }
 ///   } optional<T>;
 
-val is_not_unit: #bytes:Type0 -> {|bytes_like bytes|} -> #a:Type -> ps_a:parser_serializer_prefix bytes a -> Type0
+val is_not_unit: #bytes:Type0 -> {|bytes_like bytes|} -> #a:Type -> ps_a:parser_serializer_prefix bytes a -> prop
 
 /// We define a special type for message formats with non-extensibility and non-emptiness,
 /// because they are the most common ones we encounter in the wild.

src/Comparse.Parser.Typeclass.fst

@@ -30,7 +30,7 @@ val serialize_parse_inv_lemma: #bytes:Type0 -> {|bytes_like bytes|} -> a:Type ->
 let serialize_parse_inv_lemma #bytes #bl a #ps buf =
   ps.base.serialize_parse_inv buf
 
-val is_well_formed: #bytes:Type0 -> {|bytes_like bytes|} -> a:Type -> {|parseable_serializeable bytes a|} -> bytes_compatible_pre bytes -> a -> Type0
+val is_well_formed: #bytes:Type0 -> {|bytes_like bytes|} -> a:Type -> {|parseable_serializeable bytes a|} -> bytes_compatible_pre bytes -> a -> prop
 let is_well_formed #bytes #bl a #ps pre x =
   is_well_formed_whole ps.base pre x