1
(* Test r�gression bug #1041 *)
5
pose (P:= fun x y :Prop => y).
6
evar (Q: forall X Y,P X Y -> Prop) .
8
instantiate (1:= fun _ => _ ) in (Value of Q).
9
instantiate (1:= fun _ => _ ) in (Value of Q).
10
instantiate (1:= fun _ => _ ) in (Value of Q).
11
instantiate (1:= H) in (Value of Q).