13 | "LIST_REL R (x#xs) [] = False"

    13 | "LIST_REL R (x#xs) [] = False"

    14 | "LIST_REL R [] (x#xs) = False"

    14 | "LIST_REL R [] (x#xs) = False"

    15 | "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"

    15 | "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"

    16 

    16 

    17 lemma LIST_REL_EQ:

    17 lemma LIST_REL_EQ:

    19 unfolding expand_fun_eq

    19 unfolding expand_fun_eq

    20 apply(rule allI)+

    20 apply(rule allI)+

    21 apply(induct_tac x xa rule: list_induct2')

    21 apply(induct_tac x xa rule: list_induct2')

    22 apply(simp_all)

    22 apply(simp_all)

    23 done

    23 done