blob: 401e86649b08c94f1037ce91e9bccef4dc4954eb (
plain)
1
2
3
4
5
6
7
8
9
|
Set Primitive Projections.
Record total2 (P : nat -> Prop) := tpair { pr1 : nat; pr2 : P pr1 }.
Theorem onefiber' (q : total2 (fun y => y = 0)) : True.
Proof. assert (foo:=pr2 _ q). simpl in foo.
destruct foo. (* Error: q is used in conclusion. *) exact I. Qed.
Print onefiber'.
|
