Add emptylist

tests/emptylist.smt3

@@ -0,0 +1,31 @@
+(declare-const a Bool)
+(declare-const b Bool)
+(declare-const = (-> (! Type :var T :implicit) T T Bool))
+(declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
+(declare-const and (-> Bool Bool Bool) :right-assoc-nil true)
+
+
+(program mk_nary_cong_lhs ((U Type) (f (-> U U)) (t1 U) (t2 U) (s1 U) (s2 U)  (tail Bool :list))
+    ((-> U U) Bool) Bool
+    (
+        ((mk_nary_cong_lhs f (and (= s1 s2) tail)) (f s1 (mk_nary_cong_lhs f tail)))
+        ((mk_nary_cong_lhs f true)                 (alf.emptylist f))
+    )
+)
+(program mk_nary_cong_rhs ((U Type) (f (-> U U)) (t1 U) (t2 U) (s1 U) (s2 U)  (tail Bool :list))
+    ((-> U U) Bool) Bool
+    (
+        ((mk_nary_cong_rhs f (and (= s1 s2) tail)) (f s2 (mk_nary_cong_rhs f tail)))
+        ((mk_nary_cong_rhs f true)                 (alf.emptylist f))
+    )
+)
+
+(declare-rule nary_cong ((U Type) (E Bool) (f (-> U U)) (nil U))
+    :premise-list E and
+    :args (f)
+    :conclusion (= (mk_nary_cong_lhs f E) (mk_nary_cong_rhs f E))
+)
+
+(assume @p0 (= a b))
+
+(step @p1 (= (or a a a) (or b b b)) :rule nary_cong :premises (@p0 @p0 @p0) :args (or))