T1 == T2			T1 =@= T2			T1=T2
					rownosc scisla		strukturalna		unifikacja
	a,a				true				true				true
	a,b				false				false				false
	A,A				true				true				true
	A,B				false				true(A=g1,B=g2)		true(A=g3,B=g3) - powiazanie zmiennych
	X,a				false				false				true(X=a) - ukonkretnienie zmiennej. X staje się a
	f(A,B),f(a,X)	false				false				true (A=a, B=X) - ukonkretnianie
	f(A,B),f(C,D)	false				true				true A=C, B=D - powiązanie




MGU - najbardziej ogólny unifikator (r to sigma)
T1 = f(X,a)
T2 = f(b,X)		oba termy mają nazwę "f" i 2 argumenty, więc można je zunifikować
---
r1: X=b (pod X podstawiamy b)
T1r1 = f(b,a)
T2r1 = f(b,b)
więc a\=b (false)


T1=fu(a,X,f(g(Y)))
T2=fu(V,h(Z,V), f(Z))    fu/3 (można zunifikować)
---
r1: V=a
T1r1 = fu(a, X, f(g(Y)))
T2r2 = fu(a, h(Z,a), f(Z))
---
r2: X=h(Z,a)
T1r2 = (a, h(Z,a), f(g(Y)))
T2r2 = (a, h(Z,a), f(Z))
---
r3: f(g(Y))=f(Z)
T1r3 = (a, h(Z,a), f(Z))
T2r3 = (a, h(Z,a), f(Z))
---
MGU(T1,T2)
=r1r2r3
={V=a, Z=g(Y), X=h(Z,a)}