fact: Fixpoint unify (u:option (table (option term))) (a b:term) {struct a} : option (table (option term)) := match a,b with X i, c => add_to_unifier c i u | const s, X j => none (table (option term)) | const s, ev m n => none (table (option term)) | const s, const r => if string_compare r s then u else none (table (option term)) | ev m n, X j => none (table (option term)) | ev m n, const s => none (table (option term)) | ev m n, ev l p => match u with none => none (table (option term)) | _ => unify (unify u m l) n p end end.