Terminating map via commuting conversions

get.v

Inductive Tree (A : Set) : Set :=
  | Leaf : A -> Tree A
  | Node : bool -> Tree A * Tree A -> Tree A.

Definition subTree {A : Set} (b : bool) (lr : Tree A * Tree A) : Tree A :=
  match (b, lr) with
    | (true, (a, b)) => a
    | (false, (a, b)) => b
  end.

Fixpoint get {A : Set} (t : Tree A) : A :=
  match t with
    | Leaf _ a    => a
    | Node _ b lr => get (subTree b lr)
  end.