theory Transfer_List 
imports
  Quotient_Coinductive_List 
begin

lemma transfer_list_llist: "type_definition llist_of list_of {xs. lfinite xs}"
by unfold_locales simp_all

setup_lifting transfer_list_llist

lemma [transfer_rule]: "cr_list LNil []" 
by(simp add: cr_list_def)

lemma [transfer_rule]: "(op = ===> cr_list ===> cr_list) LCons op #"
by(rule fun_relI)+(simp add: cr_list_def)

lemma [transfer_rule]: "(cr_list ===> cr_list ===> cr_list) lappend op @"
by(rule fun_relI)+(simp add: cr_list_def)

lemma "xs @ [] = xs"
by transfer simp

lemma "lfinite xs \<Longrightarrow> lappend xs LNil = xs"
oops

end