Idris prove termination of proof without assert_smaller

Question

I am proving a theorem using Idris and in the proof, I am applying the theorem itself to the hypotheses. However, I cannot apply it the hypotheses directly; I have to do a rewrite. Because of this, Idris cannot prove it is total and so I had to use assert_smaller.

assert_smaller, however, sounds a bit like admit in Coq, and I would like a fully-verified proof.

Is it possible to prove the termination (or prove the assertation)?

Here is the code. The use of assert_smaller occurs in the second case of the theorem.

data StType = StTop
            | StTApp StType StType

data StSubtype : StType -> StType -> Type where
    S_Refl : StSubtype t t
    S_Trans : (u: StType) -> StSubtype s u -> StSubtype u t -> StSubtype s t
    S_Top : StSubtype s StTop
    S_Arrow : StSubtype t1 s1 -> StSubtype s2 t2 -> StSubtype (StTApp s1 s2) (StTApp t1 t2)

-- Theorem 
%default total
%unbound_implicits off
theorem1 : (t1, t2, s:  StType) 
        -> StSubtype s (StTApp t1 t2) 
        -> (s1: StType **
                (s2 : StType ** 
                    (s = StTApp s1 s2, 
                     StSubtype t1 s1, 
                     StSubtype s2 t2)))
theorem1 t1 t2 (StTApp t1 t2) S_Refl = (t1 ** (t2 ** (Refl, S_Refl, S_Refl)))
theorem1 t1 t2 s (S_Trans u hyp1 hyp2) = let 
    (s1 ** (s2 ** (ueq, st1, st2))) = theorem1 t1 t2 u hyp2
    hyp1' : StSubtype s (StTApp s1 s2)
    hyp1' = replace {p = id} (cong (StSubtype s) ueq) hyp1
    in case theorem1 s1 s2 s (assert_smaller (S_Trans u hyp1 hyp2) hyp1') of
        (s1' ** (s2' ** (ueq', st1', st2'))) => (s1' ** (s2' ** (ueq', S_Trans s1 st1 st1', S_Trans s2 st2' st2)))
theorem1 t1 t2 (StTApp x1 x2) (S_Arrow hyp1 hyp2) = (x1 ** (x2 ** (Refl, hyp1, hyp2)))

I searched for other solutions than assert_smaller but I could not fund!