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

[Nils Anders Danielsson]

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)

> Any advice?

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

I used the old inspect idiom, not "inspect on steroids".

-- 
/NAD