blob: 374c2cf967cdb3830595848c29e5ac7c0cafa686 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Set Implicit Arguments.
Definition hprop := nat -> Prop.
Definition himpl := fun H1 H2 : hprop => forall (h : nat), H1 h -> H2 h.
Parameter himpl_refl : forall H : hprop, himpl H H.
Parameter hstar : hprop -> hprop -> hprop.
Parameter hpure : hprop.
Lemma test : (forall (H:hprop), himpl (hstar H H) hpure -> True) -> True.
Proof. intros M. eapply M. apply himpl_refl. Abort.
|
