[[u]] 1of(e) s s' a2 tr ~ [[u]] 1of(e) s s' a1 tr
X:Top.
reduce(
t,vs. term_free_vars(t) @ vs;nil;v) = nil 
(list_accum(x,t.x([[t]] 1of(e) s s' a1 tr);X;v) ~ list_accum(x,t.x([[t]] 1of(e) s s' a2 tr);X;v))t,vs. term_free_vars(t) @ vs;nil;v)) = nil list_accum(x,t.x
([[t]] 1of(e) s s' a1 tr);X
([[u]] 1of(e) s s' a1 tr);v) ~ list_accum(x,t.x
(...);...;v)| 1 | [[u]] 1of(e) s s' a2 tr ~ [[u]] 1of(e) s s' a1 tr |
About:
 |  |  |  |  |  |  |  |  |