blob: b9a1273b1a976669b507d8a55a18278d28320b43 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Definition idw (A : Type) := A.
Lemma foobar : unit.
Proof.
Require Import Program.
apply (const tt tt).
Qed.
Set Nested Proofs Allowed.
Lemma foobar' : unit.
Lemma aux : forall A : Type, A -> unit.
Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed.
apply (@aux unit tt).
Qed.
|
