- type_rws ``:'a list``;

> val it =
    [|- (!v f. list_CASE [] v f = v) /\ !a0 a1 v f. list_CASE (a0::a1) v f = f a0 a1,
     |- !a1 a0. ~([] = a0::a1),
     |- !a1 a0. ~(a0::a1 = []),
     |- !a0 a1 a0' a1'. (a0::a1 = a0'::a1') = (a0 = a0') /\ (a1 = a1')]

- Hol_datatype `point = <| x:num ; y:num |>`;
<<HOL message: Defined type: "point">>

- type_rws ``:point``;
> val it =
    [|- !a0 a1 f. point_CASE (point a0 a1) f = f a0 a1,
     |- !a0 a1 a0' a1'. point a0 a1 = point a0' a1' <=> a0 = a0' /\ a1 = a1',
     |- !p g f.
      p with <|y updated_by f; x updated_by g|> =
      p with <|x updated_by g; y updated_by f|>,
     |- (!g f. y_fupd f o x_fupd g = x_fupd g o y_fupd f) /\
    !h g f. y_fupd f o x_fupd g o h = x_fupd g o y_fupd f o h,
     |- (!n n0. (point n n0).x = n) /\ !n n0. (point n n0).y = n0,
     |- (!p f. (p with y updated_by f).x = p.x) /\
    (!p f. (p with x updated_by f).y = p.y) /\
    (!p f. (p with x updated_by f).x = f p.x) /\
    !p f. (p with y updated_by f).y = f p.y,
     |- !p n0 n. p with <|x := n0; y := n|> = <|x := n0; y := n|>,
     |- !n01 n1 n02 n2.
      <|x := n01; y := n1|> = <|x := n02; y := n2|> <=>
      n01 = n02 /\ n1 = n2,
     |- (!p g f.
       p with <|x updated_by f; x updated_by g|> =
       p with x updated_by f o g) /\
    !p g f.
      p with <|y updated_by f; y updated_by g|> =
      p with y updated_by f o g,
     |- ((!g f. x_fupd f o x_fupd g = x_fupd (f o g)) /\
     !h g f. x_fupd f o x_fupd g o h = x_fupd (f o g) o h) /\
    (!g f. y_fupd f o y_fupd g = y_fupd (f o g)) /\
    !h g f. y_fupd f o y_fupd g o h = y_fupd (f o g) o h]