At: closed rel mng sq1121211 1. s: Top 2. e: Top 3. a1: Top 4. a2: Top 5. tr: Top 6. l: Term List 7. u: Term 8. v: Term List 9. X:Top.
reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil
(list_accum(x,t.x([[t]] 1of(e) s a1 tr);X;v) ~ list_accum(x,t.x([[t]] 1of(e) s a2 tr);X;v)) 10. X: Top 11. term_free_vars(u) = nil 12. reduce(t,vs. term_free_vars(t) @ vs;nil;v) = nil