elem : type.

list : type.
nil : list.
cons : elem -> list -> list.

list-reverse : list -> list -> list -> type.
lr/nil : list-reverse nil L L.
lr/cons : list-reverse (cons E L1) L2 L3
           <- list-reverse L1 (cons E L2) L3.
%solve test : {e1}{e2}{e3}{e4} list-reverse (cons e1 (cons e3 (cons e2 (cons e4 nil)))) nil _.