blob: 9b691e253c09d0fcf418af1318434578864cd95a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
(* Wish #2154 by E. van der Weegen *)
(* auto was not using f_equal-style lemmas with metavariables occuring
only in the type of an evar of the concl, but not directly in the
concl itself *)
Parameters
(F: Prop -> Prop)
(G: forall T, (T -> Prop) -> Type)
(L: forall A (P: A -> Prop), G A P -> forall x, F (P x))
(Q: unit -> Prop).
Hint Resolve L.
Goal G unit Q -> F (Q tt).
intro.
auto.
Qed.
(* Test implicit arguments in "using" clause *)
Goal forall n:nat, nat * nat.
auto using (pair O).
Undo.
eauto using (pair O).
Qed.
|
