From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/1754.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 test-suite/bugs/closed/1754.v (limited to 'test-suite/bugs/closed/1754.v') diff --git a/test-suite/bugs/closed/1754.v b/test-suite/bugs/closed/1754.v new file mode 100644 index 00000000..06b8dce8 --- /dev/null +++ b/test-suite/bugs/closed/1754.v @@ -0,0 +1,24 @@ +Axiom hp : Set. +Axiom cont : nat -> hp -> Prop. +Axiom sconj : (hp -> Prop) -> (hp -> Prop) -> hp -> Prop. +Axiom sconjImpl : forall h A B, + (sconj A B) h -> forall (A' B': hp -> Prop), + (forall h', A h' -> A' h') -> + (forall h', B h' -> B' h') -> + (sconj A' B') h. + +Definition cont' (h:hp) := exists y, cont y h. + +Lemma foo : forall h x y A, + (sconj (cont x) (sconj (cont y) A)) h -> + (sconj cont' (sconj cont' A)) h. +Proof. + intros h x y A H. + eapply sconjImpl. + 2:intros h' Hp'; econstructor; apply Hp'. + 2:intros h' Hp'; eapply sconjImpl. + 3:intros h'' Hp''; econstructor; apply Hp''. + 3:intros h'' Hp''; apply Hp''. + 2:apply Hp'. + clear H. +Admitted. -- cgit v1.2.3