[Agda] How to case split on the value of a function (the second time)?

[Jacques Carette]

So I have a function
sub1 : {A B : Set} → ((⊤ ⊎ A) ≃ (⊤ ⊎ B)) → A → B
which given an isomorphism as above, will extract a function A → B. Now, 
that function actually has some nice properties, which I would like to 
prove, such as

sub1congr : {A B : Set} → (eq : (⊤ ⊎ A) ≃ (⊤ ⊎ B)) → {x : A} → (((sub1 
eq) ○ (sub1 (sym≃ eq))) x ≡ x)

where sym≃ is symmetry of isomorphism. The "problem" is that sub1 is 
written as a case split on the values of the underlying isomorphism 
(i.e. eq contains a function f : (⊤ ⊎ A) → (⊤ ⊎ B) and I do a case-split 
on the range). This works for getting sub1 defined. I do need to make 
use of the 'inspect' idiom in there.

However, no matter what I do, I cannot get the goals in sub1congr to 
reduce given the same case split.

Any advice?

Jacques