- type_rws "list";

> val it =
    [|- (!v f. case v f [] = v) /\ !v f a0 a1. case v f (a0::a1) = 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 =
    [|- !f a0 a1. case f (point a0 a1) = f a0 a1,
     |- !a0 a1 a0' a1'.
          (point a0 a1 = point a0' a1') = (a0 = a0') /\ (a1 = a1'),
     |- !z x p. p with <|y := x; x := z|> = p with <|x := z; y := x|>,
     |- (!x p. (p with y := x).x = p.x) /\ (!x p. (p with x := x).y = p.y) /\
        (!x p. (p with x := x).x = x) /\ !x p. (p with y := x).y = x,
     |- (!n n0. (point n n0).x = n) /\ !n n0. (point n n0).y = n0,
     |- (!n1 n n0. point n n0 with x := n1 = point n1 n0) /\
        !n1 n n0. point n n0 with y := n1 = point n n1,
     |- (!p. p with x := p.x = p) /\ !p. p with y := p.y = p,
     |- (!x2 x1 p. p with <|x := x1; x := x2|> = p with x := x1) /\
        !x2 x1 p. p with <|y := x1; y := x2|> = p with y := x1,
     |- (!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|>]