I have no idea how to prove the following lemma. Can anyone help me with it? I wouldn't mind using classical logic. Thanks!

```
Lemma foo {I : Type} {J : I -> Type} (ix: I) (jx: J ix):
exists f : forall i : I, J i, f ix = jx.
Proof.
Admitted.
```

you can't, it's absurd

```
Lemma bad : (forall {I : Type} {J : I -> Type} (ix: I) (jx: J ix),
exists f : forall i : I, J i, f ix = jx)
-> False.
Proof.
intros F.
destruct (F bool (fun b => if b then True else False) true I) as [f _].
exact (f false).
Qed.
```

If you take `I`

to be `bool`

and `J true = True`

and `J false = False`

and `ix = true`

then `jx`

is just a proof of `True`

but you also need to provide a proof of `False`

because `f false : False`

?

I see. Thank you both!

Yu Zhang has marked this topic as resolved.

Last updated: Jun 15 2024 at 09:01 UTC