equal
deleted
inserted
replaced
367 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
367 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
368 apply(lifting concat2) |
368 apply(lifting concat2) |
369 apply(cleaning) |
369 apply(cleaning) |
370 apply (simp add: finsert_def fconcat_def comp_def) |
370 apply (simp add: finsert_def fconcat_def comp_def) |
371 apply cleaning |
371 apply cleaning |
372 (* ID PROBLEM *) |
|
373 apply(simp add: id_def[symmetric] id_simps) |
|
374 done |
372 done |
375 |
373 |
376 text {* raw section *} |
374 text {* raw section *} |
377 |
375 |
378 lemma map_rsp_aux: |
376 lemma map_rsp_aux: |