aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1754.v
blob: 06b8dce851bfe1c4d4084b5a0900732c8baee040 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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.