Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/adcacb0b7e838a73e54ae39d500f9213]
elem : type.
list : type.
nil : list.
cons : elem -> list -> list.
list-reverse : list -> list -> list -> type.
lr/nil : {L:list} list-reverse nil L L.
lr/cons :
   {L1:list} {E:elem} {L2:list} {L3:list}
      list-reverse L1 (cons E L2) L3 -> list-reverse (cons E L1) L2 L3.
%solve 
{e1:elem} {e2:elem} {e3:elem} {e4:elem}
   list-reverse (cons e1 (cons e3 (cons e2 (cons e4 nil)))) nil (X1 e1 e2 e3 e4).
 OK
test :
   {e1:elem} {e2:elem} {e3:elem} {e4:elem}
      list-reverse (cons e1 (cons e3 (cons e2 (cons e4 nil)))) nil
         (cons e4 (cons e2 (cons e3 (cons e1 nil))))
   = [e1:elem] [e2:elem] [e3:elem] [e4:elem]
        lr/cons (lr/cons (lr/cons (lr/cons lr/nil))).
[Closing file /home/www/twelfwiki/code/adcacb0b7e838a73e54ae39d500f9213]
%% OK %%