let mytheory2 = ref [
`(ZIP [] [] = []) /\ (ZIP (CONS h1 t1) (CONS h2 t2) = CONS (h1,h2) (ZIP t1 t2))`;
`~(CONS h t = [])`;
`(LAST [h:A] = h) /\ (LAST (CONS h (CONS k t)) = LAST (CONS k t))`;
`APPEND (l:A list) [] = l`;
`APPEND (l:A list) (APPEND m n) = APPEND (APPEND l m) n`;
`REVERSE (APPEND (l:A list) m) = APPEND (REVERSE m) (REVERSE l)`;
`REVERSE(REVERSE (l:A list)) = l`;
`(CONS h1 t1 = CONS h2 t2) <=> (h1 = h2) /\ (t1 = t2)`;
`LENGTH(APPEND (l:A list) (m:A list)) = LENGTH l + LENGTH m`;
`MAP (f:A->B) (APPEND l1 l2) = APPEND (MAP f l1) (MAP f l2)`;
`LENGTH (MAP (f:A->B) l) = LENGTH l`;
`(LENGTH (l:A list) = 0) <=> (l = [])`;
`(LENGTH l = SUC n) /\ (l = CONS h t) ==> (LENGTH t = n)`;
`ALL (\x. f x = g x) l ==> (MAP f l = MAP g l)`;
`(MEM x l /\ P x ==> Q x) /\ ALL P l ==> ALL Q l`;
`~(EX P l) <=> ALL (\x. ~(P x)) l`;
`~(ALL P l) <=> EX (\x. ~(P x)) l`;
`ALL P (MAP f l) <=> ALL (P o f) l`;
`ALL (\x. T) l`;
`ALL2 (\x y. f x = f y) l m ==> (MAP f l = MAP f m)`;
`ALL2 P (MAP f l) l <=> ALL (\a. P (f a) a) l`;
`ALL (\x. f(x) = x) l ==> (MAP f l = l)`;
`ALL2 (\x y. P x /\ Q x y) l m <=> ALL P l /\ ALL2 Q l m`;
`ITLIST f (APPEND l1 l2) a = ITLIST f l1 (ITLIST f l2 a)`;
`ITLIST f (APPEND l [a]) b = ITLIST f l (f a b)`;
`ALL (\x. P x ==> Q x) l /\ ALL P l ==> ALL Q l`;
`ALL P l /\ ALL Q l <=> ALL (\x. P x /\ Q x) l`;
`(MEM x l /\ P x ==> Q x) /\ EX P l ==> EX Q l`;
`(MEM x l ==> P x) <=> ALL P l`;
`LENGTH(REPLICATE n x) = n`;
`EX P (MAP f l) <=> EX (P o f) l`;
`(ALL (P x) l) <=> ALL (\s. P x s) l`;
`MEM x (APPEND l1 l2) <=> MEM x l1 \/ MEM x l2`;
`FILTER P (APPEND l1 l2) = APPEND (FILTER P l1) (FILTER P l2)`;
`FILTER P (MAP f l) = MAP f (FILTER (P o f) l)`;
`MEM x (FILTER P l) <=> P x /\ MEM x l`;
`(LENGTH l1 = LENGTH l2) ==> (MAP FST (ZIP l1 l2) = l1)`;
`(LENGTH l1 = LENGTH l2) ==> (MAP SND (ZIP l1 l2) = l2)`;
`MEM (x,ASSOC x l) l <=> MEM x (MAP FST l)`;
`ALL P (APPEND l1 l2) <=> ALL P l1 /\ ALL P l2`;
`n < LENGTH l ==> MEM (EL n l) l`;
`ALL2 P (MAP f l) (MAP g m) = ALL2 (\x y. P (f x) (g y)) l m`;
`ALL2 P l m /\ ALL2 Q l m <=> ALL2 (\x y. P x y /\ Q x y) l m`;
`ALL2 P l l <=> ALL (\x. P x x) l`;
`(APPEND l m = []) <=> (l = []) /\ (m = [])`;
`(LENGTH l = LENGTH m) ==> (LENGTH(MAP2 f l m) = LENGTH m)`;
`(P x ==> Q x) ==> ALL P l ==> ALL Q l`;
`((P:A->B->bool) x y ==> Q x y) ==> ALL2 P l l' ==> ALL2 Q l l'`
]