25
(* M and P should be closed *)
26
Lemma th1 : m = 0 /\ p = 0.
33
(* M and P should still be closed *)
34
Lemma th2 : m = 0 /\ p = 0.
40
(********************************************************************)
63
(* M and P should be closed *)
64
Lemma th1 : m = 0 /\ p = 0.
71
(* M and P should now be opened *)
72
Lemma th2 : m = 1 /\ p = 1.