| changeset 41842 | d8f76db6a207 |
| parent 34233 | 156c42518cfc |
| child 44890 | 22f665a2e91c |
| 41840:f69045fdc836 | 41842:d8f76db6a207 |
|---|---|
109 apply(rule conjI) |
109 apply(rule conjI) |
110 apply clarify |
110 apply clarify |
111 apply simp |
111 apply simp |
112 apply clarify |
112 apply clarify |
113 apply simp |
113 apply simp |
114 apply(case_tac j,simp) |
|
115 apply simp |
|
116 apply simp |
114 apply simp |
117 apply(rule conjI) |
115 apply(rule conjI) |
118 apply clarify |
116 apply clarify |
119 apply simp |
117 apply simp |
120 apply clarify |
118 apply clarify |