Removing

tests/rare-example.smt3

@@ -10,8 +10,22 @@
   (= (or xs true ys) true)
 )
 
+(program elim_singleton_list_rhs ((T Type) (f (-> T T T)) (t T) (s T :list))
+  ((-> T T T) T) T
+  (
+  ((elim_singleton_list_rhs f (f t s)) (alf.ite (alf.is_eq s (alf.emptylist f)) t (f t s)))
+  ((elim_singleton_list_rhs f t)        t)
+  )
+)(program elim_singleton_list_lhs ((T Type) (f (-> T T T)) (t T :list) (s T))
+  ((-> T T T) T) T
+  (
+  ((elim_singleton_list_lhs f (f t s)) (alf.ite (alf.is_eq t (alf.emptylist f)) s (f t s)))
+  ((elim_singleton_list_lhs f s)        s)
+  )
+)
+
 (declare-axiom bool-or-false ((xs Bool :list) (ys Bool :list))
-  (= (or xs false ys) (alf.from_list or (or xs ys)))
+  (= (or xs false ys) (elim_singleton_list_rhs or (alf.concat or xs ys)))
 )
 
 (step @p0 (= (or a b true c) true) :rule bool-or-true :args ((or a b) (or c)))
@@ -23,7 +37,7 @@
 (step @p5 (= (or (or a b) false) (or a b)) :rule bool-or-false :args ((or (or a b)) false))
 
 (declare-axiom bool-and-true ((xs Bool :list) (ys Bool :list))
-  (= (and xs true ys) (alf.from_list and (and xs ys)))
+  (= (and xs true ys) (elim_singleton_list_lhs and (alf.concat and xs ys)))
 )
 
 (declare-axiom bool-and-false ((xs Bool :list) (ys Bool :list))