diff --git a/carcara/src/translation/tests/alethe_signature/alethe.eo b/carcara/src/translation/tests/alethe_signature/alethe.eo
index 9d496cc5..49fbbeac 100644
--- a/carcara/src/translation/tests/alethe_signature/alethe.eo
+++ b/carcara/src/translation/tests/alethe_signature/alethe.eo
@@ -47,7 +47,10 @@
   :conclusion CL
 )
 
-;TODO
+;;;;;;;;;;;;;;;;;;;;;;;
+; Rule 6: th_resolution
+;;;;;;;;;;;;;;;;;;;;;;;
+; TODO
 (program check_resolution ((Cs Bool) (CL Bool))
   (Bool Bool) Bool
   (
@@ -55,14 +58,16 @@
   )
 )
 
-;TRUST
-(declare-rule th_resolution ((Cs Bool) (CL Bool))
+(declare-rule th_resolution ((Cs Bool))
   :premise-list Cs and
-  :args (CL)
-  :requires (((check_resolution Cs CL) true))
-  :conclusion CL
+  :requires (((check_resolution Cs eo::conclusion) true))
+  :conclusion-given
 )
 
+;;;;;;;;;;;;;;;;;;;;;;;
+; Rule 7: resolution
+;;;;;;;;;;;;;;;;;;;;;;;
+
 ;TRUST
 (declare-rule resolution ((Cs Bool))
   :premise-list Cs and
@@ -442,7 +447,7 @@
 (program check_and ((premise Bool) (premise_non_cl Bool) (index Int) (conclusion Bool))
   (Bool Int Bool) Bool
   (((check_and premise index conclusion)
-    (cl_equal (to_cl (index_list and (from_cl premise) index))
+    (cl_equal (to_cl (f_list_index and (from_cl premise) index))
                conclusion))
   )
 )
@@ -491,7 +496,7 @@
     (check_not_or premise_non_cl index conclusion))
 
    ((check_not_or (not disjuncts) index conclusion)
-    (cl_equal (to_cl (not (index_list or disjuncts index)))
+    (cl_equal (to_cl (not (f_list_index or disjuncts index)))
                conclusion))
    )
 )
@@ -570,7 +575,7 @@
 (program check_not_and ((conjunction Bool) (conclusion Bool))
   (Bool Bool) Bool
   (((check_not_and (not conjunction) conclusion)
-     (cl_equal (transform_not_and conjunction) conclusion)
+     (cl_equal (de_morgan_not_and conjunction) conclusion)
      )
   )
 )
@@ -877,11 +882,11 @@
   (Int Bool) Bool
   (
    ((check_and_pos pos (@cl (not antecedent) consequent))
-    (cl_equal (index_list and antecedent pos) consequent))
+    (cl_equal (f_list_index and antecedent pos) consequent))
 
    ;; To simplify the use of the checker
    ((check_and_pos pos (@cl consequent (not antecedent)))
-    (cl_equal (index_list and antecedent pos) consequent))
+    (cl_equal (f_list_index and antecedent pos) consequent))
   )
 )
 
@@ -919,7 +924,7 @@
   (Bool) Bool
   (
    ((check_and_neg (@cl left_disjunct right_disjunct))
-    (cl_equal (transform_not_and left_disjunct)
+    (cl_equal (de_morgan_not_and left_disjunct)
               right_disjunct))
   )
 )
@@ -970,10 +975,10 @@
   (Int Bool) Bool
   (
    ((check_or_neg index (@cl left_disjunct (not right_disjunct)))
-    (prop_syntax_eq (index_list or left_disjunct index) right_disjunct))
+    (prop_syntax_eq (f_list_index or left_disjunct index) right_disjunct))
    
    ((check_or_neg index (@cl (not left_disjunct) right_disjunct))
-    (prop_syntax_eq right_disjunct (index_list or left_disjunct index)))
+    (prop_syntax_eq right_disjunct (f_list_index or left_disjunct index)))
   )
 )
 
@@ -1632,18 +1637,17 @@
 )
 
 ;TODO
-(program check_prod_simplify ((l Bool) (r Bool))
-  (Bool Bool) Bool
+(program check_prod_simplify ((conclusion Bool))
+  (Bool) Bool
   (
-   ((check_prod_simplify l r) true)
+   ((check_prod_simplify conclusion) true)
   )
 )
 
 ;TRUST
-(declare-rule prod_simplify ((l Bool) (r Bool))
-  :args ((@cl (= l r)))
-  :requires (((check_prod_simplify l r) true))
-  :conclusion (@cl (= l r))
+(declare-rule prod_simplify ()
+  :requires (((check_prod_simplify eo::conclusion) true))
+  :conclusion-given
 )
 
 ;TODO
@@ -1731,30 +1735,88 @@
   :conclusion-given
 )
 
-;TODO
-(program check_distinct_elim ((l Bool) (r Bool))
+;;;;;;;;;;;;;;;;;;;;;;;;
+; Rule 93: distinct_elim
+;;;;;;;;;;;;;;;;;;;;;;;;
+
+; program: build_distinct_list_single_elem
+; args:
+; - lhs Bool:
+; - distinct_list Bool: a distinct-list
+; return:
+(program build_distinct_list_single_elem ((lhs Bool) (hd Bool) (tail Bool))
   (Bool Bool) Bool
   (
-   ((check_distinct_elim l r) true)
+   ((build_distinct_list_single_elem lhs (distinct Bool hd tail))
+    (and (not (= lhs hd)) 
+         (build_distinct_list_single_elem lhs (distinct Bool tail))))
+
+   ; { hd is single element distinct-list }
+   ((build_distinct_list_single_elem lhs (distinct Bool hd))
+    (not (= lhs hd)))
   )
 )
 
-;TRUST
-(declare-rule distinct_elim ((l Bool) (r Bool))
-  :args ((@cl (= l r)))
-  :requires (((check_distinct_elim l r) true))
-  :conclusion (@cl (= l r))
+; program: check_distinct_elim
+; args:
+; - l Bool:
+; - r Bool:
+; return:
+(program build_distinct_list_full_list ((lhs Bool) (rhs Bool) (tl Bool :list))
+  (Bool) Bool
+  (
+   ((build_distinct_list_full_list (and (distinct lhs rhs) tl
+                                        ))
+    (and (not (= lhs rhs))
+         (build_distinct_list_full_list tl)))
+
+   ; Only one proposition
+   ((build_distinct_list_full_list (distinct lhs rhs)) (not (= lhs rhs)))
+
+   ; Only one proposition
+   ((build_distinct_list_full_list (distinct lhs)) true)
+   
+   ((build_distinct_list_full_list true) true)
+  )
 )
 
-;;;;;;;;;;;;;;;;;;
-; Rule 94: and_neg
-;;;;;;;;;;;;;;;;;;
+(program check_distinct_elim ((hd Bool) (tl Bool) (conjunctions Bool))
+  (Bool) Bool
+  (
+   ((check_distinct_elim (@cl (= (distinct Bool hd tl) conjunctions)))
+    ;; (f_list_equal and 
+                  (build_distinct_list_full_list (distinct Bool hd tl))
+                  ;; conjunctions)
+                  )
+
+   ; Only one proposition
+   ((check_distinct_elim (@cl (= (distinct Bool hd) true))) true)
+  )
+)
+
+; rule: distinct_elim
+; implements: TODO?
+; premises:
+; - distinct_elim nil:
+; args:
+; requires:
+; conclusion:
+(declare-rule distinct_elim ()
+  :requires (((check_distinct_elim eo::conclusion) true))
+  :conclusion-given
+)
+
+;;;;;;;;;;;;;;;;;;;
+; Rule 94: la_rw_eq
+;;;;;;;;;;;;;;;;;;;
 
 ; program: check_la_rw_eq
 ; args:
-; - t Real:
-; - u Real:
-; return:
+; - conclusion Bool: >
+;   The conclusion provided to the la_rw_eq rule. Must be build with @cl.
+; return: >
+;   A boolean indicating if "conclusion" is a clause of the form 
+;   (= (= t u) (and (<= t u) (<= u t))), for some numbers t and u.
 (program check_la_rw_eq ((t Real) (u Real))
   (Bool) Bool
   (
@@ -1765,7 +1827,9 @@
 ; TODO: other number types. Can the equality be flipped?
 ; rule: la_rw_eq
 ; implements: TODO?
-; requires:
+; requires: >
+;   Requires for the conclusion to be a clause of the form 
+;   (= (= t u) (and (<= t u) (<= u t))), for some numbers t and u.
 ; conclusion-given: >
 ;  Only the "requires" predicate checks if a proper conclusion is given.
 (declare-rule la_rw_eq ()
diff --git a/carcara/src/translation/tests/alethe_signature/programs.eo b/carcara/src/translation/tests/alethe_signature/programs.eo
index 9fc1efe7..d5e5a6ae 100644
--- a/carcara/src/translation/tests/alethe_signature/programs.eo
+++ b/carcara/src/translation/tests/alethe_signature/programs.eo
@@ -2,6 +2,76 @@
 
 ;; Library of auxiliary programs, useful to manipulate propositions.
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; f-lists computations
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; define: f_list_index
+; args:
+; - f (-> A A A): >
+;   Right/left assoc. operator used to construct the given f-list
+;   (see definition of f-list, for a given operator f, in ethos
+;   manual: https://github.com/cvc5/ethos/blob/main/user_manual.md#list-computations)
+; - list (A): An f-list: a term of the form (f t1 ... tn)
+; - index Int: >
+;   An integer, from 0 to the number of parameters - 1 in (f t1 ... tn) 
+;   (i.e., "list)
+; return: The parameter number "index" - 1, from (f t1 ... tn) (i.e., "list")
+(program f_list_index ((A Type) (f (-> A A A)) (hd A) (tail A :list) (index Int))
+  ((-> A A A) A Int) A
+  (
+   ((f_list_index f (f hd tail) 0) hd)
+
+   ;; { index > 0 }
+   ((f_list_index f (f hd tail) index)
+    ;; TODO: using eo::add
+    (f_list_index f tail (eo::add index -1)))
+  )
+)
+
+(program f_list_contains_elem ((A Type) (f (-> A A A)) (elem A) 
+                               (hd A) (tl A :list))
+  ((-> A A A) A A) Bool
+  (
+   ((f_list_contains_elem f elem (f elem tl)) true)
+
+   ;; { head of list is not phi}
+   ((f_list_contains_elem f elem (f hd tl)) (f_list_contains_elem f elem tl))
+
+   ((f_list_contains_elem f elem elem) true)
+
+   ;; { hd != elem}
+   ((f_list_contains_elem f elem hd) false)
+  )
+)
+
+(program f_list_contains_f_list ((A Type) (f (-> A A A)) (elem A) 
+                                 (hd A) (tl A :list)
+                                 (f_list_2 A))
+  ((-> A A A) A A) Bool
+  (
+   ((f_list_contains_f_list f (@cl hd tl) f_list_2)
+    ;; TODO: I need some way to build boolean values
+    ;; combining other boolean values, but I would like
+    ;; to avoid built-in operators.
+    (eo::and (f_list_contains_elem f hd f_list_2)
+             (f_list_contains_f_list f tl f_list_2)))
+
+ 
+   ;; { f_list_1 is not a term built with f }
+   ((f_list_contains_f_list f hd f_list_2)
+    (f_list_contains_elem f hd f_list_2))
+  )
+)
+
+(program f_list_equal ((A Type) (f (-> A A A)) (f_list_1 A) (f_list_2 A))
+  ((-> A A A) A A) Bool
+  (
+   ((f_list_equal f f_list_1 f_list_2)
+    (eo::and (f_list_contains_f_list f f_list_1 f_list_2)
+             (f_list_contains_f_list f f_list_2 f_list_1)))
+  )
+)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; CLAUSES
@@ -50,49 +120,49 @@
    )
 )
 
-; program: cl_contains_prop
-; args:
-; - phi Bool: A proposition.
-; - clause Bool: A clause, built with @cl.
-; return: A boolean indicating if "phi" is a disjunct from "clause".
-(program cl_contains_prop ((phi Bool) (hd Bool) (tl Bool :list))
-  (Bool Bool) Bool
-  (
-   ((cl_contains_prop phi (@cl phi tl)) true)
-
-   ;; { head of list is not phi}
-   ((cl_contains_prop phi (@cl hd tl)) (cl_contains_prop phi tl))
-
-   ((cl_contains_prop phi phi) true)
-
-   ;; { hd != phi}
-   ((cl_contains_prop phi hd) false)
-  )
-)
-
-; program: cl_contains_cl
-; args:
-; - cl_1 Bool: A clause, built with @cl.
-; - cl_2 Bool: A clause, built with @cl.
-; return: >
-;   A boolean indicating if cl_1's disjuncts are also present
-;   in cl_2
-(program cl_contains_cl ((hd Bool) (tl Bool :list) (cl_2 Bool))
-  (Bool Bool) Bool
-  (
-   ((cl_contains_cl (@cl hd tl) cl_2)
-    ;; TODO: I need some way to build boolean values
-    ;; combining other boolean values, but I would like
-    ;; to avoid built-in operators.
-    (eo::and (cl_contains_prop hd cl_2)
-             (cl_contains_cl tl cl_2)))
+;; ; program: cl_contains_prop
+;; ; args:
+;; ; - phi Bool: A proposition.
+;; ; - clause Bool: A clause, built with @cl.
+;; ; return: A boolean indicating if "phi" is a disjunct from "clause".
+;; (program cl_contains_prop ((phi Bool) (hd Bool) (tl Bool :list))
+;;   (Bool Bool) Bool
+;;   (
+;;    ((cl_contains_prop phi (@cl phi tl)) true)
+
+;;    ;; { head of list is not phi}
+;;    ((cl_contains_prop phi (@cl hd tl)) (cl_contains_prop phi tl))
+
+;;    ((cl_contains_prop phi phi) true)
+
+;;    ;; { hd != phi}
+;;    ((cl_contains_prop phi hd) false)
+;;   )
+;; )
+
+;; ; program: cl_contains_cl
+;; ; args:
+;; ; - cl_1 Bool: A clause, built with @cl.
+;; ; - cl_2 Bool: A clause, built with @cl.
+;; ; return: >
+;; ;   A boolean indicating if cl_1's disjuncts are also present
+;; ;   in cl_2
+;; (program cl_contains_cl ((hd Bool) (tl Bool :list) (cl_2 Bool))
+;;   (Bool Bool) Bool
+;;   (
+;;    ((cl_contains_cl (@cl hd tl) cl_2)
+;;     ;; TODO: I need some way to build boolean values
+;;     ;; combining other boolean values, but I would like
+;;     ;; to avoid built-in operators.
+;;     (eo::and (cl_contains_prop hd cl_2)
+;;              (cl_contains_cl tl cl_2)))
 
  
-   ;; { cl_1 is not a clause built with @cl }
-   ((cl_contains_cl hd cl_2)
-    (cl_contains_prop hd cl_2))
-  )
-)
+;;    ;; { cl_1 is not a clause built with @cl }
+;;    ((cl_contains_cl hd cl_2)
+;;     (cl_contains_prop hd cl_2))
+;;   )
+;; )
 
 ; program: cl_equal
 ; args:
@@ -103,8 +173,10 @@
 (program cl_equal ((cl_1 Bool) (cl_2 Bool))
   (Bool Bool) Bool
   (
-   ((cl_equal cl_1 cl_2) (eo::and (cl_contains_cl cl_1 cl_2)
-                                  (cl_contains_cl cl_2 cl_1)))
+   ((cl_equal cl_1 cl_2)
+    (f_list_equal @cl cl_1 cl_2))
+    ;; (eo::and (cl_contains_cl cl_1 cl_2)
+    ;;          (cl_contains_cl cl_2 cl_1)))
   )
 )
 
@@ -132,40 +204,13 @@
 ; return: >
 ;   Applies De Morgan's law over the conjuncts of "ls", returning a new clause
 ;   built with @cl.
-(program transform_not_and ((l Bool) (ls Bool))
+(program de_morgan_not_and ((l Bool) (ls Bool))
   (Bool) Bool
   (
-   ((transform_not_and (and l ls))
-    (@cl (not l) (from_cl (transform_not_and ls)))
+   ((de_morgan_not_and (and l ls))
+    (@cl (not l) (from_cl (de_morgan_not_and ls)))
     )
 
-   ((transform_not_and l) (@cl (not l)))
-  )
-)
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; List computations
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-; define: index_list
-; args:
-; - cons (-> A A A): >
-;   Right/left assoc. operator used to construct the given cons-list
-;   (see definition of f-list, for a given operator f, in ethos
-;   manual: https://github.com/cvc5/ethos/blob/main/user_manual.md#list-computations)
-; - list (A): A cons-list: a term of the form (cons t1 ... tn)
-; - index Int: >
-;   An integer, from 0 to the number of parameters - 1 in (cons t1 ... tn) 
-;   (i.e., "list)
-; return: The parameter number "index" - 1, from (cons t1 ... tn) (i.e., "list")
-(program index_list ((A Type) (cons (-> A A A)) (hd A) (tail (-> A A)) (index Int))
-  ((-> A A A) A Int) A
-  (
-   ((index_list cons (cons hd tail) 0) hd)
-
-   ;; { index > 0 }
-   ((index_list cons (cons hd tail) index)
-    ;; TODO: using eo::add
-    (index_list cons tail (eo::add index -1)))
+   ((de_morgan_not_and l) (@cl (not l)))
   )
 )
diff --git a/carcara/src/translation/tests/gen_verit_proof_certs.sh b/carcara/src/translation/tests/gen_verit_proof_certs.sh
index b4e82288..87ccacf7 100755
--- a/carcara/src/translation/tests/gen_verit_proof_certs.sh
+++ b/carcara/src/translation/tests/gen_verit_proof_certs.sh
@@ -3,7 +3,7 @@
 # Generates Alethe proof certificates, using $COMMAND, from input problems
 # contained in $DIR.
 DIR="./verit_problems/"
-COMMAND="../../../../../verit/veriT --proof=- --disable-print-success --disable-banner --proof-prune --proof-merge"
+COMMAND="../../../../../verit_gitlab/verit/veriT --proof=- --disable-print-success --disable-banner --proof-prune --proof-merge"
 CARCARA_COMMAND="../../../../target/release/carcara check --expand-let-bindings --allow-int-real-subtyping --ignore-unknown-rules"
 
 # Loop through each file in the directory.