## Stream: Coq users

### Topic: ✔ Construct a function from a point

#### Yu Zhang (Dec 14 2021 at 15:41):

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.
``````

#### Gaëtan Gilbert (Dec 14 2021 at 15:48):

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.
``````

#### Théo Winterhalter (Dec 14 2021 at 15:49):

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`?

#### Yu Zhang (Dec 14 2021 at 15:50):

I see. Thank you both!

#### Notification Bot (Dec 14 2021 at 15:50):

Yu Zhang has marked this topic as resolved.

Last updated: Jun 15 2024 at 09:01 UTC