blob: a5de82e0d8ba4859bed0e14d342e06fbafb307db (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Goal Prop.
pose (P:=(fun x y :Prop => y)).
evar (Q: (forall X Y,P X Y -> Prop)) .
instantiate (1:= fun _ => _ ) in (Value of Q).
instantiate (1:= fun _ => _ ) in (Value of Q).
instantiate (1:= fun _ => _ ) in (Value of Q).
instantiate (1:=H) in (Value of Q).
Admitted.
|
