blob: 490e4f4b6cbd45a09877c4cf93ae56ce3f6e7ff9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Inductive box (A : Type) := Box : A -> box A.
Axiom PRED : unit -> Prop.
Axiom FUN : forall (u : unit), box (PRED u).
Axiom U : unit.
Definition V := U.
Goal match FUN U with Box _ _ => True end.
Proof.
repeat match goal with
| [ |- context G[ U ] ] =>
let e := context G [ V ] in
change e
end.
set (Z := V).
clearbody Z. (* This fails if change misses the case parameters *)
destruct (FUN Z).
constructor.
Qed.
|
