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

[Jacques Carette]

On 2013-12-08 17:22 , Nils Anders Danielsson wrote:
> On 2013-12-06 17:40, Jacques Carette wrote:
>> sub1 : {A B : Set} → ((⊤ ⊎ A) ≃ (⊤ ⊎ B)) → A → B
>> sub1congr : {A B : Set} → (eq : (⊤ ⊎ A) ≃ (⊤ ⊎ B)) → {x : A} → 
>> (((sub1 eq) ○ (sub1 (sym≃ eq))) x ≡ x)
>
> I've proved a similar property about a similar function, see
> Fin.⊎-left-cancellative:
>
> http://www.cse.chalmers.se/~nad/listings/equality/Function-universe.html#41160

That is indeed a very similar function, thanks.  I did manage to prove 
mine, using ideas [in hindsight] very similar to those you used.  Your 
proof is certainly visually much more appealing than mine -- this 
encourages me to keep optimizing my proof.

Jacques