[Agda] nontermination and Sized types

[Vlad]

Thank you all for the answers so far.

I have a further question, and I'm anxious to know the answer like my 
Agda development depended on it (which it does) : in one of the 
discussions about issues with sized types 
https://github.com/agda/agda/issues/2820 there is the following code :

data [Size<_] (i : Size) : Set where
   box : Size< i → [Size< i ]

unbox : ∀ {i} → [Size< i ] → Size< i
unbox (box j) = j

elim :
   ∀ {p}
   (P : Size → Set p) →
   (∀ i → ((j : [Size< i ]) → P (unbox j)) → P i) →
   ∀ i → P i
elim P f i = f i λ { (box j) → elim P f j }

If understand correctly, "elim" is *not* a well-founded induction 
principle on Size (which would be wrong) but something approaching it... 
which turns out to be enough for me.

Thus, I would like to know whether there is a *known* inconsistency that 
can be derived using "elim". I tried using it to prove an actual 
well-founded induction principle on Size  and that seems impossible, so 
there's at least some hope.

- Vlad