# deffun append(l1, l2) = ite(l1, <hd(l1) : append(tl(l1), l2)>, l2);
deffun append(l1, l2) =
  ite(l1, <hd(l1) : append(tl(l1), l2)>, l2)
# deffun eq(l1, l2) =
      ite(l1,
          ite(l2,
              ite(eq(hd(l1), hd(l2)),
                  ite(eq(tl(l1), tl(l2)), [*], *),
                  *),
              *),
          ite(l2, *, [*]));
deffun eq(l1, l2) =
  ite(l1, ite(l2, ite(eq(hd(l1), hd(l2)), ite(eq(tl(l1), tl(l2)), [*], *), *), *),
ite(l2, *, [*]))
# deffun dupnil(l) =
       ite(l, < ite(hd(l), dupnil(hd(l)), [*, *]) : dupnil(tl(l))>, *);
deffun dupnil(l) =
  ite(l, <ite(hd(l), dupnil(hd(l)), [*, *]) : dupnil(tl(l))>, *)
# deffun flat(l) =
  ite(l, append(ite(hd(l), flat(hd(l)), [*]), flat(tl(l))), *);
deffun flat(l) =
  ite(l, append(ite(hd(l), flat(hd(l)), [*]), flat(tl(l))), *)
# defvar a = [[*], *];
defvar a =
  [[*], *]
-> [[*], *]
# defvar b = [*, [*]];
defvar b =
  [*, [*]]
-> [*, [*]]
# defvar c = append(a, b);
defvar c =
  append(a, b)
-> [[*], *, *, [*]]
# defvar d = append(b, a);
defvar d =
  append(b, a)
-> [*, [*], [*], *]
# eval eq(c, d);
eq(c, d)
-> *
# eval eq(flat(dupnil(c)), flat(dupnil(d)));
eq(flat(dupnil(c)), flat(dupnil(d)))
-> [*]
# defvar e = <dupnil(c), dupnil(d), dupnil(c) : dupnil(d)>;
defvar e =
  <dupnil(c), dupnil(d), dupnil(c) : dupnil(d)>
-> [[[[*, *]], [*, *], [*, *], [[*, *]]], [[*, *], [[*, *]], [[*, *]], [*, *]],
[[[*, *]], [*, *], [*, *], [[*, *]]], [*, *], [[*, *]], [[*, *]], [*, *]]
# defvar f = <dupnil(d), dupnil(c), dupnil(c) : dupnil(c)>;
defvar f =
  <dupnil(d), dupnil(c), dupnil(c) : dupnil(c)>
-> [[[*, *], [[*, *]], [[*, *]], [*, *]], [[[*, *]], [*, *], [*, *], [[*, *]]],
[[[*, *]], [*, *], [*, *], [[*, *]]], [[*, *]], [*, *], [*, *], [[*, *]]]
# eval eq(flat(e), flat(f));
eq(flat(e), flat(f))
-> [*]