From fc84c27eac260dffd8f2fb1cb56d599f1e3486d9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 9 Mar 2015 11:07:53 +0100
Subject: Initial commit

---
 mathcomp/ssrtest/first_n.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 mathcomp/ssrtest/first_n.v

(limited to 'mathcomp/ssrtest/first_n.v')

diff --git a/mathcomp/ssrtest/first_n.v b/mathcomp/ssrtest/first_n.v
new file mode 100644
index 0000000..175684a
--- /dev/null
+++ b/mathcomp/ssrtest/first_n.v
@@ -0,0 +1,9 @@
+(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+Require Import ssreflect ssrbool.
+
+Lemma test : False -> (bool -> False -> True -> True) -> True.
+move=> F; let w := 2 in apply; last w first.
+- by apply: F.
+- by apply: I.
+by apply: true.
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3