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/view_case.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 mathcomp/ssrtest/view_case.v

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

diff --git a/mathcomp/ssrtest/view_case.v b/mathcomp/ssrtest/view_case.v
new file mode 100644
index 0000000..f6de3df
--- /dev/null
+++ b/mathcomp/ssrtest/view_case.v
@@ -0,0 +1,18 @@
+Require Import ssreflect ssrbool ssrnat eqtype seq fintype zmodp.
+
+Axiom P : forall T, seq T -> Prop.
+
+Goal (forall T (s : seq T), P _ s).
+move=> T s.
+elim: s => [| x /lastP [| s] IH].
+Admitted.
+
+Goal forall x : 'I_1, x = 0 :> nat.
+move=> /ord1 -> /=; exact: refl_equal.
+Qed.
+
+Goal forall x : 'I_1, x = 0 :> nat.
+move=> x.
+move=> /ord1 -> in x |- *.
+exact: refl_equal.
+Qed.
-- 
cgit v1.2.3