Idris: rewrite does not work (rewriting by ... did not change)

Question

I'm proving a theorem in Idris, and in the 2nd case:

theorem1 t1 t2 s (S_Trans u hyp1 hyp2) = let 
    (s1 ** (s2 ** (ueq, st1, st2))) = theorem1 t1 t2 u 
    hyp1' = rewrite ueq in hyp1
    in case theorem1 s1 s2 s hyp1' of
        (s1' ** (s2' ** (ueq', st1', st2'))) => (s1' ** (s2' ** (ueq', S_Trans s1 st1 st1', S_Trans s2 st2' st2)))`

hyp1 has type StSubtype s u and ueq has type u = StTApp s1 s2. I would like a term hyp1' with type StSubtype s (StTApp s1 s2).

For this, I tried rewrite ueq in hyp1, which gives an error:

Error: While processing right hand side of theorem1. Rewriting
by u = StTApp s1 s2 did not change
type ?_ [locals in scope: u, t2, t1, hyp2, s, hyp1, s1, s2, ueq, st1, st2].

If I write a type annotation for hyp1', hyp1' : StSubtype s (StTApp s1 s2), it gives a similar error:

Error: While processing right hand side of theorem1. While processing right hand
side of $resolved2797,hyp1'. Rewriting by u = StTApp s1 s2 did not change
type StSubtype s (StTApp s1 s2).```

Answer 1

Use rewrite cong (StSubtype s) (sym ueq) in hyp1

What's sym?

See this answer. In brief, rewrite needs StTApp s1 s2 = u not u = StTApp s1 s2. sym flips the equality.

What's cong?

rewrite a = b in c changes the whole of the type of c from b to a. What you want is to turn StSubtype s u into StSubtype s (StTApp s1 s2). You only have StTApp s1 s2 = u (after using sym), but need StSubtype s (StTApp s1 s2) = StSubtype s u. With

cong : (0 f : t -> u) -> (0 p : a = b) -> f a = f b

you can add the StSubtype s.