blob: 6c23baffa016a79347fca7ecd667bb2bb5b2591a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Definition something (P:Type) (e:P) := e.
Inductive myunit : Set := mytt.
(* Proof below works when definition is in Type,
however builtin types such as unit are in Set. *)
Lemma demo_hide_generic :
let x := mytt in x = x.
Proof.
intros.
change mytt with (@something _ mytt) in x.
subst x. (* Proof works if this line is removed *)
reflexivity.
Qed.
|
