let rec term_equal (term1: term) (term2: term) : bool =
term1 == term2
||
begin
match term1, term2 with
| Func func1, Func func2 ->
not (func1.in_db && func2.in_db)
&&
Symbol.equal func1.symbol func2.symbol
&&
Tools.array_for_all2
(fun term1 term2 ->
term_equal term1 term2
)
func1.subterms
func2.subterms
| _ ->
false
end