// unification
/  A. Martelli & A. Montanari, An Efficient Unification Algorithm, 
/  ACM Transactions on Programming Languages and Systems, 4(2), 1982 

v:{(_ic*$x)_in 95,65+!26}						/ x a variable?

unify:{:[x~y;();x[0]~*y;(vt fg tv vv tt@)/+(1_ x;1_ y)]}		/ find most general unifier (or _n)

tt:{:[@x;;_di[x;i],,/(+1_')'x i:&{:[|/@:'x;0;~=/#:'x;0;=/*:'x]}'x]}	/ [f T][f U] -> +[T U]
vv:{:[@x;;x _di&{(&/v'x)&~/x}'x]}					/ v v -> 
tv:{:[@x;;{(</v'x)!x}'x]}						/ t v -> v t
fg:{:[@x;;~|/{:[|/v'x;0;~~/*:'x]}'x;x]}					/ [f T][g T] -> FAIL

vt:{									/ v t -> replace
 :[@x					;				/ FAIL?
   ~#i:&{>/v'x}'x			;x				/ v t
   ~#i@:&x[i;0](|/occurs/:)'x _di/:i	;x				/ v occurs elsewhere
   ~|/occurs .'x i			;replace/[x;i]]}		/ v occurs in self -> FAIL else replace

replace:{apply[x _di y;x y],,x y}					/ replace v from v t elsewhere
apply:{:[~@x;x _f\:y;x=*y;y 1;x]}					/ apply y=[.. v t ..] in x
occurs:{:[@y;x=y;|/x _f/:y]}						/ v occurs in E