197 

   197 

   198 lemma ho_tst: "foldl my_plus x [] = x"

   198 lemma ho_tst: "foldl my_plus x [] = x"

   199 apply simp

   199 apply simp

   200 done

   200 done

   201 

   201 

   202 lemma "foldl PLUS x [] = x"

   204 lemma "foldl PLUS x [] = x"

   203 apply(lifting ho_tst)

   205 apply(lifting ho_tst)

   204 done

   206 done

   205 

   207 

   206 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"

   208 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"