1326 lemma 

  1326 lemma 

  1327   shows "fconcat {||} = {||}"

  1327   shows "fconcat {||} = {||}"

  1328 apply(lifting_setup concat.simps(1))

  1328 apply(lifting_setup concat.simps(1))

  1329 apply(rule test)

  1329 apply(rule test)

  1330 apply(tactic {* resolve_tac (Quotient_Info.equiv_rules_get @{context}) 1 *})

  1330 apply(tactic {* resolve_tac (Quotient_Info.equiv_rules_get @{context}) 1 *})

  1331 sorry

  1332 sorry

  1332 

  1333 

  1333 lemma fconcat_insert:

  1334 lemma fconcat_insert:

  1334   shows "fconcat (finsert x S) = x |\<union>| fconcat S"

  1335   shows "fconcat (finsert x S) = x |\<union>| fconcat S"

  1335   by (lifting concat.simps(2))

  1336   by (lifting concat.simps(2))