blob: 3c0b81568afbaffffa2df1da547769bd09d8cb11 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Definition idw (A : Type) := A.
Lemma foobar : unit.
Proof.
Require Import Program.
apply (const tt tt).
Qed.
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.
|
