I'm attempting to do that as follows:
λ (A : *) ->
λ (B : (A -> *)) ->
λ (t : (∀ (r : *) -> (∀ (x : a) -> (B x) -> r)) -> r) ->
(t (B (t A (λ (x : A) -> λ (y : (B x)) -> x)))
(λ (x : A) -> λ (y : (B x)) -> y))
Notice that, since the value returned by that function depends on a value inside the sigma itself, I need to extract that value. This code doesn't check, because, I believe, it fails to unify the type extracted from Sigma with the type inside it.
Is there any workaround?