fact: Definition unify_cumul {A B} (x: A) (y: B) : t bool := of <- unify_univ A B; match of with | Some f => let fx := f x in oeq <- unify fx y; match oeq with Some _ => ret true | None => ret false end | None => ret false end.