diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1041.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1041.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1041.v b/test-suite/bugs/closed/shouldsucceed/1041.v new file mode 100644 index 00000000..a5de82e0 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1041.v @@ -0,0 +1,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. + |