From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 test-suite/bugs/closed/HoTT_coq_047.v | 46 +++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 test-suite/bugs/closed/HoTT_coq_047.v

(limited to 'test-suite/bugs/closed/HoTT_coq_047.v')

diff --git a/test-suite/bugs/closed/HoTT_coq_047.v b/test-suite/bugs/closed/HoTT_coq_047.v
new file mode 100644
index 00000000..29496be5
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_047.v
@@ -0,0 +1,46 @@
+Inductive nCk : nat -> nat -> Type :=
+  |zz : nCk 0 0
+  | incl { m n : nat } : nCk m n -> nCk (S m) (S n)
+  | excl { m n : nat } : nCk m n -> nCk (S m) n.
+
+Definition nCkComp { l m n : nat } :
+  nCk l m -> nCk m n -> nCk l n.
+Proof.
+  intro.
+  revert n.
+  induction H.
+  auto.
+(* ( incl w ) o zz -> contradiction *)
+  intros.
+    remember (S n) as sn.
+    destruct H0.
+      discriminate Heqsn.
+    apply incl.
+      apply IHnCk.
+      injection Heqsn.
+      intro.
+      rewrite <- H1.
+      auto.
+    apply excl.
+      apply IHnCk.
+      injection Heqsn.
+      intro. rewrite <- H1.
+      auto.
+  intros.
+  apply excl.
+  apply IHnCk.
+  auto.
+Defined.
+
+Lemma nCkEq { k l m n : nat } ( cs : nCk k l ) (ct : nCk l m) (cr : nCk m n ):
+  nCkComp cs (nCkComp ct cr) = nCkComp (nCkComp cs ct) cr.
+Proof.
+  revert m n ct cr.
+  induction cs.
+  intros. simpl. auto.
+  intros.
+  destruct n.
+   destruct m0.
+    destruct n0.
+     destruct cr.
+(* Anomaly: Evar ?nnn was not declared. Please report. *)
-- 
cgit v1.2.3