[Agda] Standard WellFounded

[Sergei Meshveliani]

Dear all,

I am trying to understand how to use WellFounded of Standard library.

Can anybody demonstrate it on the following example?

--------------------------------------------------------------
open import Function  using (_∘_)
open import Data.List using (List; []; _∷_)
open import Data.Bin  using (Bin; toBits; pred)

open Bin

predBin : Bin → Bin
predBin = pred ∘ toBits

downFrom : Bin → List Bin     -- x ∷ x-1 ∷ x-2 ∷ ... ∷ 0# ∷ []
downFrom 0#      =  0# ∷ []
downFrom (bs 1#) =  (bs 1#) ∷ (downFrom (predBin (bs 1#)))
--------------------------------------------------------------

downFrom  is not recognized as terminating.
How to reorganize it with using items from  
Induction/*, WellFounded.agda ?

Thanks,

------
Sergei