datatype 'a Tree =
    Lf
  | Br of 'a * 'a Tree * 'a Tree
;

val t1 = Br(2, Br(1, Lf, Lf), Br(3, Lf, Lf));

fun foldTree f u Lf = u
  | foldTree f u (Br(a, left, right)) =
      f a (foldTree f u left) (foldTree f u right)
;

fun revBranch a left right = Br(a, right, left);

local
    val reflect = foldTree revBranch Lf;
in 
    val refl_t1 = reflect t1;
end