197 unfolding Quotient_alt_def |
197 unfolding Quotient_alt_def |
198 apply simp |
198 apply simp |
199 apply safe |
199 apply safe |
200 apply (drule Abs1, simp) |
200 apply (drule Abs1, simp) |
201 apply (erule Abs2) |
201 apply (erule Abs2) |
202 apply (rule pred_compI) |
202 apply (rule relcomppI) |
203 apply (rule Rep1) |
203 apply (rule Rep1) |
204 apply (rule Rep2) |
204 apply (rule Rep2) |
205 apply (rule pred_compI, assumption) |
205 apply (rule relcomppI, assumption) |
206 apply (drule Abs1, simp) |
206 apply (drule Abs1, simp) |
207 apply (clarsimp simp add: R2) |
207 apply (clarsimp simp add: R2) |
208 apply (rule pred_compI, assumption) |
208 apply (rule relcomppI, assumption) |
209 apply (drule Abs1, simp)+ |
209 apply (drule Abs1, simp)+ |
210 apply (clarsimp simp add: R2) |
210 apply (clarsimp simp add: R2) |
211 apply (drule Abs1, simp)+ |
211 apply (drule Abs1, simp)+ |
212 apply (clarsimp simp add: R2) |
212 apply (clarsimp simp add: R2) |
213 apply (rule pred_compI, assumption) |
213 apply (rule relcomppI, assumption) |
214 apply (rule pred_compI [rotated]) |
214 apply (rule relcomppI [rotated]) |
215 apply (erule conversepI) |
215 apply (erule conversepI) |
216 apply (drule Abs1, simp)+ |
216 apply (drule Abs1, simp)+ |
217 apply (simp add: R2) |
217 apply (simp add: R2) |
218 done |
218 done |
219 qed |
219 qed |