some agda that obviously terminates, but not to agda

TerminationFail.agda

postulate
  A : Set
  _≤_ : A → A → Set
  ⊥ : A
  _∨_ : A → A → A
  id : ∀{a} → a ≤ a
  _•_ : ∀{a b c} → a ≤ b → b ≤ c → a ≤ c

data Tree : Set where
  empty : Tree
  leaf : (x : A) -> Tree
  node : (l r : Tree) -> Tree

data _⊑_ : Tree → Tree → Set where
  tree• : ∀{a b c} → a ⊑ b → b ⊑ c → a ⊑ c
  -- In my actual use case I'd add more constructors here, but just tree•
  -- suffices to demonstrate the issue.

record Fun : Set where
  field ap : Tree → A
  field map : ∀{T U} → T ⊑ U → ap T ≤ ap U
open Fun

-- Consider the following definitions, or and Or.
or : Tree → A
or empty = ⊥
or (leaf x) = x
or (node T U) = or T ∨ or U

Or : Fun
ap Or = or
map Or (tree• T≤U U≤V) = map Or T≤U • map Or U≤V

-- If I try to combine these into a single definition, termination checking
-- fails. Why? :(
Or' : Fun
ap Or' empty = ⊥
ap Or' (leaf x) = x
ap Or' (node T U) = ap Or' T ∨ ap Or' U
map Or' (tree• T≤U U≤V) = map Or' T≤U • map Or' U≤V