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.
|
