From d088d13e9e1fe1928dff7e385433d95a4493c26c Mon Sep 17 00:00:00 2001
From: bodeveix <bodeveix@irit.fr>
Date: Wed, 1 Jul 2026 14:39:14 +0200
Subject: [PATCH 01/10] cond rules

---
 src/core/term.ml        |  1 +
 src/core/term.mli       |  1 +
 src/core/tree.ml        | 50 ++++++++++++++++++++++++++++++++++-------
 src/core/tree_type.ml   |  7 ++++++
 src/export/rawdk.ml     |  9 +++++---
 src/handle/inductive.ml |  2 +-
 src/parsing/dkRule.ml   |  2 +-
 src/parsing/lpLexer.ml  |  2 ++
 src/parsing/lpParser.ml | 16 ++++++++++---
 src/parsing/pretty.ml   |  9 +++++---
 src/parsing/scope.ml    |  9 +++++++-
 src/parsing/syntax.ml   | 24 +++++++++++++++-----
 12 files changed, 106 insertions(+), 26 deletions(-)

diff --git a/src/core/term.ml b/src/core/term.ml
index 1791c8b57..875bd70b4 100644
--- a/src/core/term.ml
+++ b/src/core/term.ml
@@ -214,6 +214,7 @@ and sym =
   { lhs      : term list (** Left hand side (LHS). *)
   ; names    : string array (** Names of pattern variables. *)
   ; rhs      : term (** Right hand side (RHS). *)
+  ; r_when   : (term * term) option (** conditional rule constraint. *)
   ; arity    : int (** Required number of arguments to be applicable. *)
   ; arities  : int array
   (** Arities of the pattern variables bound in the RHS. *)
diff --git a/src/core/term.mli b/src/core/term.mli
index 5af110b65..ea56db1b5 100644
--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -146,6 +146,7 @@ and rule =
   { lhs      : term list (** Left hand side (LHS). *)
   ; names    : string array (** Names of pattern variables. *)
   ; rhs      : term (** Right hand side (RHS). *)
+  ; r_when   : (term * term) option (** conditional rule constraint. *)
   ; arity    : int (** Required number of arguments to be applicable. *)
   ; arities  : int array
   (** Arities of the pattern variables bound in the RHS. *)
diff --git a/src/core/tree.ml b/src/core/tree.ml
index dfbe2190e..6816b3f6f 100644
--- a/src/core/tree.ml
+++ b/src/core/tree.ml
@@ -71,6 +71,13 @@ module CP = struct
       let compare = Stdlib.compare
     end)
 
+  (** Functional sets of pairs of terms. *)
+  module TSet = Set.Make(
+    struct
+      type t = (psym * pvar list) * (psym * pvar list)
+      let compare = Stdlib.compare
+    end)
+
   (** A pool of (convertibility and free variable) conditions. *)
   type t =
     { variables : pvar IntMap.t
@@ -85,17 +92,23 @@ module CP = struct
     ; fv_conds : int array IntMap.t
     (** A mapping of [i] to [xs] represents a free variable condition that can
         only be satisfied if only the free variables of [x] appear in the term
-        stored at slot [i] in the [vars] array of [Eval.tree_walk]. *) }
+        stored at slot [i] in the [vars] array of [Eval.tree_walk]. *)
+    ; eq_conds : TSet.t
+    (** Set of pairs of terms that should be convertible. *)
+    }
 
   (** [empty] is the condition pool holding no condition. *)
   let empty : t =
     { variables = IntMap.empty
     ; nl_conds = PSet.empty
-    ; fv_conds = IntMap.empty }
+    ; fv_conds = IntMap.empty
+    ; eq_conds = TSet.empty }
 
   (** [is_empty pool] tells whether the pool of constraints is empty. *)
   let is_empty : t -> bool = fun pool ->
-    PSet.is_empty pool.nl_conds && IntMap.is_empty pool.fv_conds
+    PSet.is_empty pool.nl_conds
+    && IntMap.is_empty pool.fv_conds
+    && TSet.is_empty pool.eq_conds
 
   (** [register_nl i (slot,vs) pool] registers the fact that the slot [slot]
       in the [vars] array correspond to a term stored at index [i] in the
@@ -119,6 +132,11 @@ module CP = struct
   let register_fv : int -> int array -> t -> t = fun i vs pool ->
     { pool with fv_conds = IntMap.add i vs pool.fv_conds }
 
+  (** [register_eq t1 t2 pool] registers a convertibility constraint
+      between terms [t1] and [t2] in [pool]. *)
+  let register_eq : (psym * pvar list) -> (psym * pvar list) -> t -> t = fun t1 t2 pool ->
+    { pool with eq_conds = TSet.add (t1,t2) pool.eq_conds }
+  
   (** [constrained_nl i pool] tells whether index [i] in the RHS's environment
       has already been associated to a variable of the [vars] array. *)
   let constrained_nl : int -> t -> bool = fun slot pool ->
@@ -129,6 +147,8 @@ module CP = struct
   let is_contained : tree_cond -> t -> bool = fun cond pool ->
     match cond with
     | CondNL(i,j) -> PSet.mem (i,j) pool.nl_conds
+    | CondEQ(t1,t2) -> TSet.mem (t1,t2) pool.eq_conds
+                       || TSet.mem (t2,t1) pool.eq_conds
     | CondFV(i,x) ->
         try Array.eq (=) x (IntMap.find i pool.fv_conds)
         with Not_found -> false
@@ -137,6 +157,7 @@ module CP = struct
   let remove cond pool =
     match cond with
     | CondNL(i,j)  -> {pool with nl_conds = PSet.remove (i,j) pool.nl_conds}
+    | CondEQ(t1,t2) -> {pool with eq_conds = TSet.remove (t1,t2) pool.eq_conds}
     | CondFV(i,xs) ->
         try
           let ys = IntMap.find i pool.fv_conds in
@@ -161,8 +182,18 @@ module CP = struct
       | p :: ps -> try Some(export (IntMap.choose p.fv_conds))
                    with Not_found -> choose_vf ps
     in
+    let rec choose_eq pools =
+      let export (t1,t2) = CondEQ(t1,t2) in
+      match pools with
+      | []      -> None
+      | p :: ps -> try Some(export (TSet.choose p.eq_conds))
+                   with Not_found -> choose_eq ps
+    in
     let res = choose_nl pools in
-    if res = None then choose_vf pools else res
+    if res = None then
+      let res = choose_eq pools in
+      if res = None then choose_vf pools else res
+    else res
 end
 
 (** {1 Clause matrix and pattern matching problem} *)
@@ -224,6 +255,8 @@ module CM = struct
     (** Left hand side of a rule. *)
     ; c_rhs       : rule
     (** Right hand side of a rule, and number of extra variables. *)
+    ; c_when      : (term * term) option
+    (** convertibility constraint for conditional rules *)
     ; c_subst     : rhs_substit
     (** Substitution of RHS variables. *)
     ; xvars_nb    : int
@@ -290,9 +323,10 @@ module CM = struct
 
   (** [of_rules rs] transforms rewriting rules [rs] into a clause matrix. *)
   let of_rules : rule list -> t = fun rs ->
-    let r2r ({lhs; xvars_nb; _} as c_rhs) =
+    let r2r ({lhs; xvars_nb; r_when; _} as c_rhs) =
       let c_lhs = Array.of_list lhs in
-      { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb }
+      let c_when = r_when in
+      { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb; c_when }
     in
     let size = (* Get length of longest rule *)
       if rs = [] then 0 else
@@ -357,7 +391,7 @@ module CM = struct
   (** [is_exhausted p c] tells whether clause [r] whose terms are at positions
       in [p] can be applied or not. *)
   let is_exhausted : arg list -> clause -> bool =
-    fun positions {c_lhs = lhs ; cond_pool ; _} ->
+    fun positions {c_lhs = lhs ; cond_pool ; c_when; _} ->
     let nonl lhs =
       (* Verify that there are no non linearity constraints in the remaining
          terms.  We must check that there are no constraints in the remaining
@@ -384,7 +418,7 @@ module CM = struct
       in
       Array.for_all2 check lhs de && nonl lhs
     in
-    CP.is_empty cond_pool && (lhs = [||] || ripe lhs)
+    c_when = None && CP.is_empty cond_pool && (lhs = [||] || ripe lhs)
 
   (** [yield m] returns the next operation to carry out on matrix [m], that
       is, either specialising, solving a constraint or rewriting to a rule. *)
diff --git a/src/core/tree_type.ml b/src/core/tree_type.ml
index c2d7d17a2..127d69d1e 100644
--- a/src/core/tree_type.ml
+++ b/src/core/tree_type.ml
@@ -6,6 +6,7 @@ open Common
 (** {3 Atomic pattern constructor representation} *)
 
 type pvar = int * int array
+type psym = Path.t * string
 
 (** Representation of an atomic pattern constructor. *)
 module TC =
@@ -56,6 +57,8 @@ type tree_cond =
   | CondFV of pvar
   (** Are the (indexed) bound variables (which are free at the time of the
       checking) of the term at the given index in the array? *)
+  | CondEQ of (psym * pvar list) * (psym * pvar list)
+  (** user rule condition: are the two terms equivalent *)
 
 (** {b NOTE} that when performing a [tree_cond.CondFV] check, we
     are concerned about variables that were bound in the term being reduced
@@ -69,6 +72,10 @@ let tree_cond : tree_cond pp = fun ppf tc ->
       out ppf "Nl(%d[%a],%d[%a])"
         i (Array.pp int ",") xs j (Array.pp int ",") ys
   | CondFV(i, _) -> out ppf "Fv(%d)" i
+  | CondEQ((s1,a1), (s2,a2)) ->
+      out ppf "Eq(%s(%a),%s(%a))"
+        (snd s1) (List.pp int ",") (List.map fst a1)
+        (snd s2) (List.pp int ",") (List.map fst a2)
 
 (** Substitution of variables in a RHS. During the filtering process, some
     subterms of the filtered term may be stored in an array. Let [v] be that
diff --git a/src/export/rawdk.ml b/src/export/rawdk.ml
index b9b917e67..42f94fb8d 100644
--- a/src/export/rawdk.ml
+++ b/src/export/rawdk.ml
@@ -135,9 +135,12 @@ let rec remove_wraps ({elt;_} as t) =
 
 let rule : p_rule pp =
   let varset ppf set = List.pp string ", " ppf (StrSet.elements set) in
-  fun ppf {elt=(l,r);_} ->
-  out ppf "[%a] %a --> %a.@."
-    varset (pvars_lhs l) term (remove_wraps l) term r
+  fun ppf {elt=(l,r,w);_} ->
+  if w = None then
+    out ppf "[%a] %a --> %a.@."
+      varset (pvars_lhs l) term (remove_wraps l) term r
+  else
+    fatal None "Cannot translate conditional rules."
 
 type modifiers
   = prop list * expo list * match_strat list * p_modifier_aux list
diff --git a/src/handle/inductive.ml b/src/handle/inductive.ml
index ff2eaa2bd..3e6d2beb2 100644
--- a/src/handle/inductive.ml
+++ b/src/handle/inductive.ml
@@ -347,7 +347,7 @@ let iter_rec_rules :
     let nonrec_dom _ _ next = next in
     let codom xs rhs _ ts =
       let cons_arg = P.appl_list (P.iden cons_sym.sym_name) (List.rev xs) in
-      Pos.make rules_pos (arec ind_sym ts cons_arg, rhs)
+      Pos.make rules_pos (arec ind_sym ts cons_arg, rhs, None)
     in
     fold_cons_type pos ind_pred_map "" ind_sym vs cons_sym inj_var
       init aux acc_rec_dom rec_dom acc_nonrec_dom nonrec_dom codom
diff --git a/src/parsing/dkRule.ml b/src/parsing/dkRule.ml
index 09d709a20..65e78eb3f 100644
--- a/src/parsing/dkRule.ml
+++ b/src/parsing/dkRule.ml
@@ -155,4 +155,4 @@ let to_p_rule : p_dk_rule -> p_rule = fun r ->
   (* NOTE the computation order is important for setting arities properly. *)
   let lhs = build [] lhs in
   let rhs = build [] rhs in
-  Pos.make r.pos (lhs, rhs)
+  Pos.make r.pos (lhs, rhs, None)
diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml
index 21832f264..47acb2380 100644
--- a/src/parsing/lpLexer.ml
+++ b/src/parsing/lpLexer.ml
@@ -93,6 +93,7 @@ type token =
   | TYPE_TERM
   | UNIF_RULE
   | VERBOSE
+  | WHEN
   | WHY3
   | WITH
 
@@ -298,6 +299,7 @@ let rec token ~allow_rocq_syntax lb =
   | "TYPE" -> TYPE_TERM
   | "unif_rule" -> UNIF_RULE
   | "verbose" -> VERBOSE
+  | "when" -> WHEN
   | "why3" -> WHY3
   | "with" -> WITH
 
diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml
index 911372e3d..cdfc6d433 100644
--- a/src/parsing/lpParser.ml
+++ b/src/parsing/lpParser.ml
@@ -115,6 +115,7 @@ let string_of_token = function
   | UNIF_RULE -> "unif_rule"
   | VBAR -> "|"
   | VERBOSE -> "verbose"
+  | WHEN -> "when"
   | WHY3 -> "why3"
   | WITH -> "with"
 
@@ -531,7 +532,7 @@ let rec command pos1 (p_sym_mod:p_modifier list) (lb:'token lexbuf) :
       let (en, es) = List.(hd es, tl es) in
       let cat e es = P.appl (P.appl cons e) es in
       let rhs = List.fold_right cat es en in
-      let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs) in
+      let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs, None) in
       extend_pos lb (*__FUNCTION__*) pos1 (P_unif_rule(r))
   | COERCE_RULE ->
       if p_sym_mod <> [] then expected lb "" [SYMBOL]; (*or modifiers*)
@@ -686,13 +687,22 @@ and notation (lb:'token lexbuf): string Term.notation =
   | _ ->
       expected lb "" [INFIX;POSTFIX;PREFIX;QUANTIFIER]
 
-and rule (lb:'token lexbuf): (p_term * p_term) loc =
+and rule (lb:'token lexbuf): (p_term * p_term * (p_term * p_term) option) loc =
   if log_enabled() then log "%s" __FUNCTION__;
   let pos1 = current_pos lb in
   let l = term lb in
+  let w =
+    if (current_token lb == WHEN) then begin
+        consume WHEN lb;
+        let t1 = term lb in
+        consume EQUIV lb;
+        let t2 = term lb in
+        Some (t1,t2)
+      end
+    else None in 
   consume HOOK_ARROW lb;
   let r = term lb in
-  extend_pos lb (*__FUNCTION__*) pos1 (l, r)
+  extend_pos lb (*__FUNCTION__*) pos1 (l, r, w)
 
 and equation (lb:'token lexbuf): p_term * p_term =
   if log_enabled() then log "%s" __FUNCTION__;
diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml
index 759eb0bfd..a313de2ef 100644
--- a/src/parsing/pretty.ml
+++ b/src/parsing/pretty.ml
@@ -187,8 +187,11 @@ and params_list : p_params list pp = fun ppf ->
 and typ : p_term option pp = fun ppf t ->
   Option.iter (out ppf "@ : %a" term) t
 
-let rule : string -> p_rule pp = fun kw ppf {elt=(l,r);_} ->
-  out ppf "%s %a ↪ %a" kw term l term r
+let rule : string -> p_rule pp = fun kw ppf {elt=(l,r,w);_} ->
+  match w with
+  | None -> out ppf "%s %a ↪ %a" kw term l term r
+  | Some (t1,t2) -> out ppf "%s %a when %a ≡ %a ↪ %a"
+                      kw term l term t1 term t2 term r
 
 let inductive : string -> p_inductive pp =
   let cons ppf (id,a) = out ppf "@,| %a : %a" ident id term a in
@@ -214,7 +217,7 @@ let rec unpack : p_term -> (p_term * p_term) list = fun eqs ->
       else assert false
   | _ -> assert false
 
-let unif_rule : p_rule pp = fun ppf {elt=(l,r);_} ->
+let unif_rule : p_rule pp = fun ppf {elt=(l,r,_);_} ->
   let lhs =
     match Syntax.p_get_args l with
     | (_, [t; u]) -> (t, u)
diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
index def6973a5..7d1c82c3a 100644
--- a/src/parsing/scope.ml
+++ b/src/parsing/scope.ml
@@ -547,13 +547,19 @@ let patt_vars : p_term -> (string * int) list * string list =
 let scope_rule :
   ?find_sym:find_sym -> bool -> sig_state -> p_rule -> sym_rule =
   fun ?(find_sym=Sig_state.find_sym) ur ss
-      { elt = (p_lhs, p_rhs); pos = rule_pos} ->
+      { elt = (p_lhs, p_rhs, p_when); pos = rule_pos} ->
   (* Compute the set of pattern variables on both sides. *)
   let (pvs_lhs, nl) = patt_vars p_lhs in
   (* NOTE to reject non-left-linear rules check [nl = []] here. *)
   let (pvs_rhs, _ ) = patt_vars p_rhs in
   (* Check that pattern variables of RHS that are in the LHS have the right
      arity. *)
+  let pvs_when =
+    match p_when with
+    | None -> []
+    | Some (t1,t2) ->
+        let (p1,_) = patt_vars t1 and (p2,_) = patt_vars t2 in
+        p1 @ p2 in
   let check_arity (m,i) =
     try
       let j = List.assoc m pvs_lhs in
@@ -561,6 +567,7 @@ let scope_rule :
     with Not_found -> ()
   in
   List.iter check_arity pvs_rhs;
+  List.iter check_arity pvs_when;
   (* [get_root t] returns the symbol at the root of the p_term [t]. *)
   let rec get_root t = get_root_after_pratt (Pratt.parse ~find_sym ss [] t)
   and get_root_after_pratt t =
diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml
index 18bef499a..6cbcada8f 100644
--- a/src/parsing/syntax.ml
+++ b/src/parsing/syntax.ml
@@ -134,7 +134,7 @@ let rec pvars_lhs : p_term -> StrSet.t = fun {elt;pos} ->
     -> pvars_lhs u
 
 (** Parser-level rewriting rule representation. *)
-type p_rule_aux = p_term * p_term
+type p_rule_aux = p_term * p_term * (p_term * p_term) option
 type p_rule = p_rule_aux loc
 
 (** Parser-level inductive type representation. *)
@@ -182,7 +182,8 @@ module P  = struct
   let abst_list : p_ident option list -> p_term -> p_term = fun idopts t ->
     List.fold_right abst idopts t
 
-  let rule : p_term -> p_term -> p_rule = fun l r -> Pos.none (l,r)
+  let rule : p_term -> p_term -> (p_term * p_term) option -> p_rule =
+    fun l r w -> Pos.none (l,r,w)
 end
 
 (** Rewrite patterns as in Coq/SSReflect. See "A Small Scale
@@ -402,8 +403,13 @@ and eq_p_params : p_params eq = fun (i1,ao1,b1) (i2,ao2,b2) ->
   List.eq (Option.eq eq_p_ident) i1 i2
   && Option.eq eq_p_term ao1 ao2 && b1 = b2
 
-let eq_p_rule : p_rule eq = fun {elt=(l1,r1);_} {elt=(l2,r2);_} ->
-  eq_p_term l1 l2 && eq_p_term r1 r2
+let pair_eq: 'a eq -> 'b eq -> ('a * 'b) eq = fun eq1 eq2 (x1,y1) (x2,y2) ->
+  eq1 x1 x2 && eq2 y1 y2
+
+let eq_p_rule : p_rule eq = fun {elt=(l1,r1,w1);_} {elt=(l2,r2,w2);_} ->
+  eq_p_term l1 l2
+  && eq_p_term r1 r2
+  && Option.eq (pair_eq eq_p_term eq_p_term) w1 w2
 
 let eq_p_inductive : p_inductive eq =
   let eq_cons (i1,t1) (i2,t2) = eq_p_ident i1 i2 && eq_p_term t1 t2 in
@@ -616,8 +622,14 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a =
 
   let fold_term : 'a -> p_term -> 'a = fold_term_vars StrSet.empty in
 
-  let fold_rule : 'a -> p_rule -> 'a = fun a {elt=(l,r);_} ->
-    fold_term (fold_term a l) r
+  let fold_when : 'a -> (p_term * p_term) option -> 'a = fun a w ->
+    match w with
+    | Some (t1,t2) -> fold_term (fold_term a t1) t2
+    | None -> a
+  in
+
+  let fold_rule : 'a -> p_rule -> 'a = fun a {elt=(l,r,w);_} ->
+    fold_when (fold_term (fold_term a l) r) w
   in
 
   let fold_rwpatt_vars : StrSet.t -> 'a -> p_rwpatt -> 'a = fun vs a p ->

From e8b0b985fc96c1bd95c731a605471b9b4d1673d9 Mon Sep 17 00:00:00 2001
From: bodeveix <bodeveix@irit.fr>
Date: Wed, 1 Jul 2026 21:51:08 +0200
Subject: [PATCH 02/10] conditional rules

---
 src/core/coercion.ml      |  2 +-
 src/core/eval.ml          | 15 +++++++++++++
 src/core/term.ml          |  2 +-
 src/core/term.mli         |  2 +-
 src/core/tree.ml          | 45 ++++++++++++++++++++++++++++++++-------
 src/parsing/scope.ml      | 16 +++++++++++++-
 src/tool/lcr.ml           |  4 ++--
 src/tool/tree_graphviz.ml |  4 ++++
 8 files changed, 76 insertions(+), 14 deletions(-)

diff --git a/src/core/coercion.ml b/src/core/coercion.ml
index 3faf8bb5b..8f9a7cffe 100644
--- a/src/core/coercion.ml
+++ b/src/core/coercion.ml
@@ -15,6 +15,6 @@ let _ =
     and t = mk_Patt (Some 1, "t", [||]) in
     let lhs = [a;a;t] and arities = [|0;0|] and names = [|"A";"t"|] in
     { lhs; names; rhs=t; arity=3; arities; vars_nb=2; xvars_nb = 0;
-      rule_pos = None }
+      rule_pos = None; r_when = None }
   in
   Sign.add_rule Ghost.sign (coerce, rule)
diff --git a/src/core/eval.ml b/src/core/eval.ml
index 0eaf29c56..083c29309 100644
--- a/src/core/eval.ml
+++ b/src/core/eval.ml
@@ -342,6 +342,21 @@ and tree_walk : config -> sym -> stack -> (term * stack) option =
               let vi = Array.map (fun id -> mk_Vari (var id)) vi in
               let tj = msubst bj vi in
               if eq_modulo whnf cfg vars.(i) tj then ok else fail
+          | CondEQ(((p1,o1) as op1,a1), ((p2,o2) as op2,a2)) ->
+              let v1 = List.map (fun (i,_) -> vars.(i)) a1 in
+              let v2 = List.map (fun (i,_) -> vars.(i)) a2 in
+              if Logger.log_enabled() then
+                log_rew "%aCondEQ(%s[%a],%s[%a]) : %s(%a) == %s(%a)"
+                  D.depth !depth
+                  (snd op1) (List.pp D.int ",") (List.map fst a1)
+                  (snd op2) (List.pp D.int ",") (List.map fst a2)
+                  (snd op1) (List.pp Raw.term ",") v1 
+                  (snd op2) (List.pp Raw.term ",") v2;
+              let s1 = Sign.find_qualified p1 o1 in
+              let s2 = Sign.find_qualified p2 o2 in
+              let t1 = add_args (mk_Symb s1) v1 in
+              let t2 = add_args (mk_Symb s2) v2 in
+              if eq_modulo whnf cfg t1 t2 then ok else fail
           | CondFV(i,xs) ->
               let allowed =
                 (* Variables that are allowed in the term. *)
diff --git a/src/core/term.ml b/src/core/term.ml
index 875bd70b4..0f36c6102 100644
--- a/src/core/term.ml
+++ b/src/core/term.ml
@@ -214,7 +214,7 @@ and sym =
   { lhs      : term list (** Left hand side (LHS). *)
   ; names    : string array (** Names of pattern variables. *)
   ; rhs      : term (** Right hand side (RHS). *)
-  ; r_when   : (term * term) option (** conditional rule constraint. *)
+  ; r_when   : ((sym * int list) * (sym * int list)) option (** conditional rule constraint. *)
   ; arity    : int (** Required number of arguments to be applicable. *)
   ; arities  : int array
   (** Arities of the pattern variables bound in the RHS. *)
diff --git a/src/core/term.mli b/src/core/term.mli
index ea56db1b5..16a5e6925 100644
--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -146,7 +146,7 @@ and rule =
   { lhs      : term list (** Left hand side (LHS). *)
   ; names    : string array (** Names of pattern variables. *)
   ; rhs      : term (** Right hand side (RHS). *)
-  ; r_when   : (term * term) option (** conditional rule constraint. *)
+  ; r_when   : ((sym * int list) * (sym * int list)) option (** conditional rule constraint. *)
   ; arity    : int (** Required number of arguments to be applicable. *)
   ; arities  : int array
   (** Arities of the pattern variables bound in the RHS. *)
diff --git a/src/core/tree.ml b/src/core/tree.ml
index 6816b3f6f..b71ee05f4 100644
--- a/src/core/tree.ml
+++ b/src/core/tree.ml
@@ -71,7 +71,7 @@ module CP = struct
       let compare = Stdlib.compare
     end)
 
-  (** Functional sets of pairs of terms. *)
+  (** Functional sets of pairs of flat terms. *)
   module TSet = Set.Make(
     struct
       type t = (psym * pvar list) * (psym * pvar list)
@@ -134,8 +134,11 @@ module CP = struct
 
   (** [register_eq t1 t2 pool] registers a convertibility constraint
       between terms [t1] and [t2] in [pool]. *)
-  let register_eq : (psym * pvar list) -> (psym * pvar list) -> t -> t = fun t1 t2 pool ->
-    { pool with eq_conds = TSet.add (t1,t2) pool.eq_conds }
+  let register_eq : (psym * int list) -> (psym * int list) -> t -> t = 
+    fun (s1,a1) (s2,a2) pool ->
+    let pv1 = List.map (fun i -> IntMap.find i pool.variables) a1 in
+    let pv2 = List.map (fun i -> IntMap.find i pool.variables) a2 in
+    { pool with eq_conds = TSet.add ((s1,pv1),(s2,pv2)) pool.eq_conds }
   
   (** [constrained_nl i pool] tells whether index [i] in the RHS's environment
       has already been associated to a variable of the [vars] array. *)
@@ -183,10 +186,14 @@ module CP = struct
                    with Not_found -> choose_vf ps
     in
     let rec choose_eq pools =
-      let export (t1,t2) = CondEQ(t1,t2) in
+      let export vars (((_,a1) as t1), ((_,a2) as t2)) = 
+        if List.for_all (fun (i,_) -> IntMap.mem i vars) a1
+           && List.for_all (fun (i,_) -> IntMap.mem i vars) a2 then
+          CondEQ(t1,t2) 
+        else raise Not_found in
       match pools with
       | []      -> None
-      | p :: ps -> try Some(export (TSet.choose p.eq_conds))
+      | p :: ps -> try Some(export p.variables (TSet.choose p.eq_conds))
                    with Not_found -> choose_eq ps
     in
     let res = choose_nl pools in
@@ -255,7 +262,7 @@ module CM = struct
     (** Left hand side of a rule. *)
     ; c_rhs       : rule
     (** Right hand side of a rule, and number of extra variables. *)
-    ; c_when      : (term * term) option
+    ; c_when      : ((psym * int list) * (psym * int list)) option
     (** convertibility constraint for conditional rules *)
     ; c_subst     : rhs_substit
     (** Substitution of RHS variables. *)
@@ -325,7 +332,11 @@ module CM = struct
   let of_rules : rule list -> t = fun rs ->
     let r2r ({lhs; xvars_nb; r_when; _} as c_rhs) =
       let c_lhs = Array.of_list lhs in
-      let c_when = r_when in
+      let c_when = match r_when with
+        | None -> None
+        | Some ((s1,a1),(s2,a2)) ->
+            Some (((s1.sym_path,s1.sym_name), a1),
+                  ((s2.sym_path,s2.sym_name), a2)) in
       { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb; c_when }
     in
     let size = (* Get length of longest rule *)
@@ -516,6 +527,24 @@ module CM = struct
               CP.register_nl i (mem,vs) cond_pool
           | None    -> cond_pool
         in
+        let c_when, cond_pool =
+          match r.c_rhs.r_when with
+          | None -> r.c_when, cond_pool
+          | Some ((op1,a1), (op2,a2)) when
+                 List.for_all (fun i -> IntMap.mem i cond_pool.variables) a1
+                 && List.for_all (fun i -> IntMap.mem i cond_pool.variables) a2 ->
+              if Logger.log_enabled () then
+                log "Registering user constraint on position [%a] \
+                     %s %a == %s %a"
+                  arg_path a.arg_path
+                  op1.sym_name (List.pp int " ") a1
+                  op2.sym_name (List.pp int " ") a2;
+              None, CP.register_eq
+                      ((op1.sym_path,op1.sym_name), a1)
+                      ((op2.sym_path,op2.sym_name), a2)
+                      cond_pool
+          | _ -> r.c_when, cond_pool
+        in
         let c_subst =
           (* REVIEW: patterns may have slots in the RHS although they are not
              bound. *)
@@ -533,7 +562,7 @@ module CM = struct
               (mem, (i,vs)) :: r.c_subst
           | _ -> r.c_subst
         in
-        {r with c_subst; cond_pool}
+        {r with c_subst; cond_pool; c_when}
     | _ -> r
 
   (** [specialize free_vars pat col pos cls] filters and transforms LHS of
diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
index 7d1c82c3a..5a17e9974 100644
--- a/src/parsing/scope.ml
+++ b/src/parsing/scope.ml
@@ -630,7 +630,21 @@ let scope_rule :
   let arity = List.length lhs in
   let f i = try Hashtbl.find names i with Not_found -> string_of_int i in
   let names = Array.init vars_nb f in
-  let r = {lhs; names; rhs; arity; arities; vars_nb; xvars_nb; rule_pos} in
+  let pw2rw t =
+    let asPatt t = match unfold t with
+      | Patt (Some i, _, [||]) -> i
+      | _ -> fatal rule_pos "arguments should be patterns in condition [%a]."
+               term t in
+    let t = scope ~find_sym 0 mode ss Env.empty t in
+    match get_args t with
+      Symb s, args ->  (s, List.map asPatt args)
+    | _ -> fatal rule_pos "function should be a global symbol in [%a]." term t
+  in 
+  let r_when = match p_when with
+    | None -> None
+    | Some (t1,t2) -> Some (pw2rw t1, pw2rw t2) in
+  let r = {lhs; names; rhs; arity; arities; vars_nb; xvars_nb;
+           rule_pos; r_when} in
   (sym,r)
 
 (** [scope_pattern ss env t] turns a parser-level term [t] into an actual term
diff --git a/src/tool/lcr.ml b/src/tool/lcr.ml
index 42719d12b..d70323b97 100644
--- a/src/tool/lcr.ml
+++ b/src/tool/lcr.ml
@@ -55,7 +55,7 @@ let is_definable : sym -> bool = fun s ->
 (** [rule_of_def s d] creates the rule [s --> d]. *)
 let rule_of_def : sym -> term -> rule = fun s rhs ->
   {lhs=[]; names=[||]; rhs; arity=0; arities=[||]; vars_nb=0; xvars_nb=0;
-   rule_pos=s.sym_pos}
+   rule_pos=s.sym_pos; r_when = None}
 
 (** [replace t p u] replaces the subterm of [t] at position [p] by [u]. *)
 let replace : term -> subterm_pos -> term -> term = fun t p u ->
@@ -457,7 +457,7 @@ let typability_constraints : Pos.popt -> term -> subs option = fun pos t ->
     match get_args_len l with
     | Symb s, lhs, arity ->
       let r = {lhs; names=[||]; rhs; arity; arities=[||]; vars_nb=0;
-               xvars_nb=0; rule_pos=Some(new_rule_id())} in
+               xvars_nb=0; rule_pos=Some(new_rule_id()); r_when = None} in
       Some (s,r)
     | _ -> None
   in
diff --git a/src/tool/tree_graphviz.ml b/src/tool/tree_graphviz.ml
index 3097edf56..4af09c70c 100644
--- a/src/tool/tree_graphviz.ml
+++ b/src/tool/tree_graphviz.ml
@@ -46,6 +46,10 @@ let tree_to_dot : Format.formatter -> _ dtree -> unit = fun ppf dtree ->
       | CondNL((i,vi), (j,vj)) ->
           out ppf "%d[%a] ≡ %d[%a]" i ar vi j ar vj
       | CondFV(i,vs) -> out ppf "%a ⊆ FV(%d)" ar vs i
+      | CondEQ(((_p1,s1),a1), ((_p2,s2),a2)) ->
+          out ppf "%s[%a] ≡ %s[%a]"
+            s1 (List.pp int ",") (List.map fst a1)
+            s2 (List.pp int ",") (List.map fst a2)
     in
     let node_count = ref 0 in
     (* [write_tree n u v] writes tree [v] obtained from tree number [n] with a

From 38ea2e75aaafb2590cbf80bff9ee09a528c6e474 Mon Sep 17 00:00:00 2001
From: bodeveix <bodeveix@irit.fr>
Date: Wed, 1 Jul 2026 22:07:42 +0200
Subject: [PATCH 03/10] sanity_checks

---
 src/core/eval.ml        |  2 +-
 src/core/term.ml        |  3 ++-
 src/core/term.mli       |  7 ++++---
 src/core/tree.ml        | 15 ++++++++-------
 src/parsing/lpParser.ml |  5 +++--
 src/parsing/scope.ml    |  2 +-
 6 files changed, 19 insertions(+), 15 deletions(-)

diff --git a/src/core/eval.ml b/src/core/eval.ml
index 083c29309..e154756e2 100644
--- a/src/core/eval.ml
+++ b/src/core/eval.ml
@@ -350,7 +350,7 @@ and tree_walk : config -> sym -> stack -> (term * stack) option =
                   D.depth !depth
                   (snd op1) (List.pp D.int ",") (List.map fst a1)
                   (snd op2) (List.pp D.int ",") (List.map fst a2)
-                  (snd op1) (List.pp Raw.term ",") v1 
+                  (snd op1) (List.pp Raw.term ",") v1
                   (snd op2) (List.pp Raw.term ",") v2;
               let s1 = Sign.find_qualified p1 o1 in
               let s2 = Sign.find_qualified p2 o2 in
diff --git a/src/core/term.ml b/src/core/term.ml
index 0f36c6102..76614350a 100644
--- a/src/core/term.ml
+++ b/src/core/term.ml
@@ -214,7 +214,8 @@ and sym =
   { lhs      : term list (** Left hand side (LHS). *)
   ; names    : string array (** Names of pattern variables. *)
   ; rhs      : term (** Right hand side (RHS). *)
-  ; r_when   : ((sym * int list) * (sym * int list)) option (** conditional rule constraint. *)
+  ; r_when   : ((sym * int list) * (sym * int list)) option
+  (** conditional rule constraint. *)
   ; arity    : int (** Required number of arguments to be applicable. *)
   ; arities  : int array
   (** Arities of the pattern variables bound in the RHS. *)
diff --git a/src/core/term.mli b/src/core/term.mli
index 16a5e6925..086e51abe 100644
--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -146,7 +146,8 @@ and rule =
   { lhs      : term list (** Left hand side (LHS). *)
   ; names    : string array (** Names of pattern variables. *)
   ; rhs      : term (** Right hand side (RHS). *)
-  ; r_when   : ((sym * int list) * (sym * int list)) option (** conditional rule constraint. *)
+  ; r_when   : ((sym * int list) * (sym * int list)) option
+  (** conditional rule constraint. *)
   ; arity    : int (** Required number of arguments to be applicable. *)
   ; arities  : int array
   (** Arities of the pattern variables bound in the RHS. *)
@@ -176,8 +177,8 @@ and rule =
        concrete syntax) are represented in the same way, and with a unique
        name (in the rule) that is generated automatically.
 
-    Then, the term [f t u v w] matches the LHS with a substitution represented
-    by an array of terms [a] of length 3 if we
+    Then, the term [f t u v w] matches the LHS with a substitution
+    represented by an array of terms [a] of length 3 if we
     have [a.(0) = t], [a.(1) = u], [a.(1) = v] and [a.(2) = w].
 
     {b TODO} memorising [w] in the substitution is sub-optimal. In practice,
diff --git a/src/core/tree.ml b/src/core/tree.ml
index b71ee05f4..7245b291a 100644
--- a/src/core/tree.ml
+++ b/src/core/tree.ml
@@ -134,12 +134,12 @@ module CP = struct
 
   (** [register_eq t1 t2 pool] registers a convertibility constraint
       between terms [t1] and [t2] in [pool]. *)
-  let register_eq : (psym * int list) -> (psym * int list) -> t -> t = 
+  let register_eq : (psym * int list) -> (psym * int list) -> t -> t =
     fun (s1,a1) (s2,a2) pool ->
     let pv1 = List.map (fun i -> IntMap.find i pool.variables) a1 in
     let pv2 = List.map (fun i -> IntMap.find i pool.variables) a2 in
     { pool with eq_conds = TSet.add ((s1,pv1),(s2,pv2)) pool.eq_conds }
-  
+
   (** [constrained_nl i pool] tells whether index [i] in the RHS's environment
       has already been associated to a variable of the [vars] array. *)
   let constrained_nl : int -> t -> bool = fun slot pool ->
@@ -160,7 +160,7 @@ module CP = struct
   let remove cond pool =
     match cond with
     | CondNL(i,j)  -> {pool with nl_conds = PSet.remove (i,j) pool.nl_conds}
-    | CondEQ(t1,t2) -> {pool with eq_conds = TSet.remove (t1,t2) pool.eq_conds}
+    | CondEQ(t,u) -> {pool with eq_conds = TSet.remove (t,u) pool.eq_conds}
     | CondFV(i,xs) ->
         try
           let ys = IntMap.find i pool.fv_conds in
@@ -186,10 +186,10 @@ module CP = struct
                    with Not_found -> choose_vf ps
     in
     let rec choose_eq pools =
-      let export vars (((_,a1) as t1), ((_,a2) as t2)) = 
+      let export vars (((_,a1) as t1), ((_,a2) as t2)) =
         if List.for_all (fun (i,_) -> IntMap.mem i vars) a1
            && List.for_all (fun (i,_) -> IntMap.mem i vars) a2 then
-          CondEQ(t1,t2) 
+          CondEQ(t1,t2)
         else raise Not_found in
       match pools with
       | []      -> None
@@ -528,11 +528,12 @@ module CM = struct
           | None    -> cond_pool
         in
         let c_when, cond_pool =
+          let vars = cond_pool.variables in
           match r.c_rhs.r_when with
           | None -> r.c_when, cond_pool
           | Some ((op1,a1), (op2,a2)) when
-                 List.for_all (fun i -> IntMap.mem i cond_pool.variables) a1
-                 && List.for_all (fun i -> IntMap.mem i cond_pool.variables) a2 ->
+                 List.for_all (fun i -> IntMap.mem i vars) a1
+                 && List.for_all (fun i -> IntMap.mem i vars) a2 ->
               if Logger.log_enabled () then
                 log "Registering user constraint on position [%a] \
                      %s %a == %s %a"
diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml
index 6c7f6092c..b524f207e 100644
--- a/src/parsing/lpParser.ml
+++ b/src/parsing/lpParser.ml
@@ -688,7 +688,8 @@ and notation (lb:'token lexbuf): string Term.notation =
   | _ ->
       expected lb "" [INFIX;POSTFIX;PREFIX;QUANTIFIER]
 
-and rule (lb:'token lexbuf): (p_term * p_term * (p_term * p_term) option) loc =
+and rule (lb:'token lexbuf):
+      (p_term * p_term * (p_term * p_term) option) loc =
   if log_enabled() then log "%s" __FUNCTION__;
   let pos1 = current_pos lb in
   let l = term lb in
@@ -700,7 +701,7 @@ and rule (lb:'token lexbuf): (p_term * p_term * (p_term * p_term) option) loc =
         let t2 = term lb in
         Some (t1,t2)
       end
-    else None in 
+    else None in
   consume HOOK_ARROW lb;
   let r = term lb in
   extend_pos lb (*__FUNCTION__*) pos1 (l, r, w)
diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
index 5a17e9974..e544a98a2 100644
--- a/src/parsing/scope.ml
+++ b/src/parsing/scope.ml
@@ -639,7 +639,7 @@ let scope_rule :
     match get_args t with
       Symb s, args ->  (s, List.map asPatt args)
     | _ -> fatal rule_pos "function should be a global symbol in [%a]." term t
-  in 
+  in
   let r_when = match p_when with
     | None -> None
     | Some (t1,t2) -> Some (pw2rw t1, pw2rw t2) in

From dfc7053bb2bd5641fe3993820472120bb81cca5d Mon Sep 17 00:00:00 2001
From: bodeveix <bodeveix@irit.fr>
Date: Thu, 2 Jul 2026 21:32:08 +0200
Subject: [PATCH 04/10] editors

---
 CHANGES.md                                 |  1 +
 doc/lambdapi.bnf                           |  1 +
 editors/emacs/lambdapi-smie.el             |  6 ++++--
 editors/emacs/lambdapi-vars.el             |  1 +
 editors/vim/syntax/lambdapi.vim            |  2 ++
 editors/vscode/syntaxes/lp.tmLanguage.json |  2 +-
 misc/lambdapi.tex                          |  2 +-
 tests/OK/cond_rules.lp                     | 18 ++++++++++++++++++
 8 files changed, 29 insertions(+), 4 deletions(-)
 create mode 100644 tests/OK/cond_rules.lp

diff --git a/CHANGES.md b/CHANGES.md
index 88f13201b..d8fc07916 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -22,6 +22,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Tactic `#print` to print a symbol or the current goal.
 - Export to Lean.
 - Tactic `all_hyps t` calls parameterized tactic term t on all hypotheses ignoring failing calls.
+- Conditional rules `l when t1 ≡ t2 ↪ r`
 
 ### Changed
 
diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf
index 57b19e549..e3f0444ff 100644
--- a/doc/lambdapi.bnf
+++ b/doc/lambdapi.bnf
@@ -33,6 +33,7 @@
 <constructor> ::= <uid> <param_list>* ":" <term>
 
 <rule> ::= <term> "↪" <term>
+         | <term> when <term> ≡ <term> "↪" <term>
 
 <unif_rule> ::= <equation> "↪" "[" <equation> (";" <equation>)* "]"
 
diff --git a/editors/emacs/lambdapi-smie.el b/editors/emacs/lambdapi-smie.el
index 2b9ad2b30..6d42f46a6 100644
--- a/editors/emacs/lambdapi-smie.el
+++ b/editors/emacs/lambdapi-smie.el
@@ -56,7 +56,8 @@
      "rule"
      "symbol"
      "unif_rule"
-     "verbose")
+     "verbose"
+     "when")
    lambdapi--queries)
   "Commands at top level.")
 
@@ -142,7 +143,8 @@ Indent by `lambdapi-indent-basic' in proofs, and 0 otherwise."
       (symdec ("symbol" args ":" sterm))
       (indcons (args ":" sterm) ("|" args ":" sterm))
       (inddec (inddec "with" args ":" sterm "≔" indcons))
-      (rules (rules "with" sterm "↪" sterm))
+      (rules (rules "with" sterm "↪" sterm)
+             (rules "with" sterm "when" sterm "≡" sterm "↪" sterm))
       (command
                ("begin" prfcontent "abort" ";")
                ("begin" prfcontent "admitted" ";")
diff --git a/editors/emacs/lambdapi-vars.el b/editors/emacs/lambdapi-vars.el
index d5f54afdb..5271515d3 100644
--- a/editors/emacs/lambdapi-vars.el
+++ b/editors/emacs/lambdapi-vars.el
@@ -47,6 +47,7 @@
     "rule"
     "symbol"
     "unif_rule"
+    "when"
     "with")
   "Commands that enrich the signature.")
 
diff --git a/editors/vim/syntax/lambdapi.vim b/editors/vim/syntax/lambdapi.vim
index 4e485eb42..ebef338c9 100644
--- a/editors/vim/syntax/lambdapi.vim
+++ b/editors/vim/syntax/lambdapi.vim
@@ -98,6 +98,7 @@ syntax keyword KeywordOK contained type
 syntax keyword KeywordOK contained TYPE
 syntax keyword KeywordOK contained unif_rule
 syntax keyword KeywordOK contained verbose
+syntax keyword KeywordOK contained when
 syntax keyword KeywordOK contained why3
 syntax keyword KeywordOK contained with
 highlight link KeywordOK Keyword
@@ -172,6 +173,7 @@ syntax keyword KeywordKO contained type
 syntax keyword KeywordKO contained TYPE
 syntax keyword KeywordKO contained unif_rule
 syntax keyword KeywordKO contained verbose
+syntax keyword KeywordKO contained when
 syntax keyword KeywordKO contained why3
 syntax keyword KeywordKO contained with
 highlight link KeywordKO Error
diff --git a/editors/vscode/syntaxes/lp.tmLanguage.json b/editors/vscode/syntaxes/lp.tmLanguage.json
index e7a25f740..bbf5d44ff 100644
--- a/editors/vscode/syntaxes/lp.tmLanguage.json
+++ b/editors/vscode/syntaxes/lp.tmLanguage.json
@@ -45,7 +45,7 @@
     },
 
     "signature-commands": {
-      "match": "(coerce_rule|inductive|rule|symbol|unif_rule|with)\\s+([^\\s+]*)",
+      "match": "(coerce_rule|inductive|rule|symbol|unif_rule|with|when)\\s+([^\\s+]*)",
       "captures": {
         "1": {"name": "storage.type.lp"},
         "2": {"name": "entity.name.function.theorem.lp"}
diff --git a/misc/lambdapi.tex b/misc/lambdapi.tex
index 02d29e67b..090e25789 100644
--- a/misc/lambdapi.tex
+++ b/misc/lambdapi.tex
@@ -9,7 +9,7 @@
   tabsize=2,
   basicstyle={\ttfamily\small\upshape},
   backgroundcolor=\color{lightgrey},
-  keywords={abort,admit,admitted,all_hyps,apply,as,assert,assertnot,associative,assume,assumption,begin,builtin,change,commutative,compute,constant,debug,end,eval,fail,flag,first_hyp,focus,generalize,have,in,induction,inductive,infix,injective,left,let,notation,off,on,opaque,open,orelse,prefix,print,private,proofterm,protected,prover,prover_timeout,quantifier,refine,reflexivity,repeat,require,rewrite,right,rule,sequential,set,simplify,solve,symbol,symmetry,type,TYPE,unif_rule,verbose,why3,with},
+  keywords={abort,admit,admitted,all_hyps,apply,as,assert,assertnot,associative,assume,assumption,begin,builtin,change,commutative,compute,constant,debug,end,eval,fail,flag,first_hyp,focus,generalize,have,in,induction,inductive,infix,injective,left,let,notation,off,on,opaque,open,orelse,prefix,print,private,proofterm,protected,prover,prover_timeout,quantifier,refine,reflexivity,repeat,require,rewrite,right,rule,sequential,set,simplify,solve,symbol,symmetry,type,TYPE,unif_rule,verbose,why3,with,when},
   sensitive=true,
   keywordstyle=\color{blue},
   morecomment=[l]{//},
diff --git a/tests/OK/cond_rules.lp b/tests/OK/cond_rules.lp
new file mode 100644
index 000000000..4c50b840c
--- /dev/null
+++ b/tests/OK/cond_rules.lp
@@ -0,0 +1,18 @@
+symbol Prop: TYPE;
+symbol ∧: Prop → Prop → Prop;
+notation ∧ infix right 7;
+constant symbol ⊤ : Prop;
+constant symbol ⊥ : Prop;
+symbol simp: Prop → Prop;
+symbol simp1: Prop → Prop → Prop;
+
+sequential symbol subterm: Prop → Prop → Prop;
+rule subterm $p $p ↪ ⊤
+with subterm $p ($p ∧ $q) ↪ ⊤
+with subterm $p (_ ∧ $q) ↪ subterm $p $q
+with subterm _ _ ↪ ⊥;
+
+rule simp ($p ∧ ⊤) ↪ $p;
+rule simp ($p ∧ $q ∧ $r) when subterm $p $r ≡ ⊤ ↪ simp1 $p $r;
+
+assert p q r ⊢ (simp (p ∧ q ∧ p ∧ r)) ≡ simp1 p (p ∧ r);

From 944470d19a2626aeca6c6a00ffaa7792dadb8d20 Mon Sep 17 00:00:00 2001
From: bodeveix <bodeveix@irit.fr>
Date: Thu, 2 Jul 2026 21:59:21 +0200
Subject: [PATCH 05/10] exclude cond_rules

---
 tests/export_dk.sh     | 2 ++
 tests/export_raw_dk.sh | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/tests/export_dk.sh b/tests/export_dk.sh
index 741967625..e30ed6590 100755
--- a/tests/export_dk.sh
+++ b/tests/export_dk.sh
@@ -49,6 +49,8 @@ do
         Tactic|1374);;
         # use Tactic
         first_hyp|all_hyps);;
+        # use cond rules
+        cond_rules);;
         # requires an excluded file
         assume|first_hyp);;
         # default case
diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh
index 860ea29cb..40965bfdf 100755
--- a/tests/export_raw_dk.sh
+++ b/tests/export_raw_dk.sh
@@ -58,6 +58,8 @@ do
         require_nondkmident);;
         # module alias
         alias);;
+        # conditional rules
+        cond_rules);;
         # proofs
         why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp|all_hyps);;
         # "open"

From 409d1d0938250fb35ab2ce403547d37df5cd0e60 Mon Sep 17 00:00:00 2001
From: bodeveix <bodeveix@irit.fr>
Date: Fri, 3 Jul 2026 11:41:41 +0200
Subject: [PATCH 06/10] change example

---
 src/core/tree.ml       |  8 ++------
 src/parsing/scope.ml   |  2 +-
 tests/OK/cond_rules.lp | 22 ++++++++++++----------
 3 files changed, 15 insertions(+), 17 deletions(-)

diff --git a/src/core/tree.ml b/src/core/tree.ml
index 7245b291a..7f768a3f3 100644
--- a/src/core/tree.ml
+++ b/src/core/tree.ml
@@ -186,14 +186,10 @@ module CP = struct
                    with Not_found -> choose_vf ps
     in
     let rec choose_eq pools =
-      let export vars (((_,a1) as t1), ((_,a2) as t2)) =
-        if List.for_all (fun (i,_) -> IntMap.mem i vars) a1
-           && List.for_all (fun (i,_) -> IntMap.mem i vars) a2 then
-          CondEQ(t1,t2)
-        else raise Not_found in
+      let export (t1, t2) = CondEQ(t1,t2) in
       match pools with
       | []      -> None
-      | p :: ps -> try Some(export p.variables (TSet.choose p.eq_conds))
+      | p :: ps -> try Some(export (TSet.choose p.eq_conds))
                    with Not_found -> choose_eq ps
     in
     let res = choose_nl pools in
diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
index e544a98a2..9493bc62d 100644
--- a/src/parsing/scope.ml
+++ b/src/parsing/scope.ml
@@ -599,7 +599,7 @@ let scope_rule :
            ; m_lhs_arities = Hashtbl.create 7
            ; m_lhs_names   = Hashtbl.create 7
            ; m_lhs_size    = 0
-           ; m_lhs_in_env  = nl @ List.map fst pvs_rhs }
+           ; m_lhs_in_env  = nl @ List.map fst pvs_rhs @ List.map fst pvs_when}
     in
     let lhs = scope ~find_sym 0 mode ss Env.empty p_lhs in
     match mode with
diff --git a/tests/OK/cond_rules.lp b/tests/OK/cond_rules.lp
index 4c50b840c..0402de7e0 100644
--- a/tests/OK/cond_rules.lp
+++ b/tests/OK/cond_rules.lp
@@ -3,16 +3,18 @@ symbol ∧: Prop → Prop → Prop;
 notation ∧ infix right 7;
 constant symbol ⊤ : Prop;
 constant symbol ⊥ : Prop;
-symbol simp: Prop → Prop;
-symbol simp1: Prop → Prop → Prop;
 
-sequential symbol subterm: Prop → Prop → Prop;
-rule subterm $p $p ↪ ⊤
-with subterm $p ($p ∧ $q) ↪ ⊤
-with subterm $p (_ ∧ $q) ↪ subterm $p $q
-with subterm _ _ ↪ ⊥;
+sequential symbol doubles_in_and : Prop → Prop;
+sequential symbol occurs_in_and : Prop → Prop → Prop;
 
-rule simp ($p ∧ ⊤) ↪ $p;
-rule simp ($p ∧ $q ∧ $r) when subterm $p $r ≡ ⊤ ↪ simp1 $p $r;
+rule doubles_in_and ($p ∧ $q) when occurs_in_and $p $q ≡ ⊤ ↪ ⊤
+with doubles_in_and (_ ∧ $q) ↪ doubles_in_and $q
+with doubles_in_and _ ↪ ⊥;
 
-assert p q r ⊢ (simp (p ∧ q ∧ p ∧ r)) ≡ simp1 p (p ∧ r);
+rule occurs_in_and $p $p ↪ ⊤
+with occurs_in_and $p ($p ∧ _) ↪ ⊤
+with occurs_in_and $p (_ ∧ $q) ↪ occurs_in_and $p $q
+with occurs_in_and _ _ ↪ ⊥;
+
+assert p q r ⊢ doubles_in_and (p ∧ q ∧ r) ≡ ⊥;
+assert p q r ⊢ doubles_in_and (p ∧ q ∧ p ∧ r) ≡ ⊤;

From b1a6f11999f4c6ea189deb185186a31f48108ff6 Mon Sep 17 00:00:00 2001
From: bodeveix <bodeveix@irit.fr>
Date: Fri, 3 Jul 2026 11:44:01 +0200
Subject: [PATCH 07/10] long line

---
 src/parsing/scope.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
index 9493bc62d..f94c1a6ae 100644
--- a/src/parsing/scope.ml
+++ b/src/parsing/scope.ml
@@ -599,7 +599,8 @@ let scope_rule :
            ; m_lhs_arities = Hashtbl.create 7
            ; m_lhs_names   = Hashtbl.create 7
            ; m_lhs_size    = 0
-           ; m_lhs_in_env  = nl @ List.map fst pvs_rhs @ List.map fst pvs_when}
+           ; m_lhs_in_env  =
+               nl @ List.map fst pvs_rhs @ List.map fst pvs_when}
     in
     let lhs = scope ~find_sym 0 mode ss Env.empty p_lhs in
     match mode with

From bb35eaf234e7397bb8bba535872ad7ab8cdca1d9 Mon Sep 17 00:00:00 2001
From: bodeveix <bodeveix@irit.fr>
Date: Tue, 7 Jul 2026 16:12:46 +0200
Subject: [PATCH 08/10] add subterm conditions in rules

---
 doc/lambdapi.bnf                |  5 ++-
 editors/emacs/lambdapi-smie.el  |  5 ++-
 editors/emacs/lambdapi-vars.el  |  1 +
 editors/vim/syntax/lambdapi.vim |  2 +
 misc/lambdapi.tex               |  1 +
 src/core/coercion.ml            |  2 +-
 src/core/eval.ml                | 12 ++++++
 src/core/term.ml                | 11 ++++-
 src/core/term.mli               | 11 ++++-
 src/core/tree.ml                | 72 +++++++++++++++++++++++++++------
 src/core/tree_type.ml           |  4 ++
 src/export/rawdk.ml             |  2 +-
 src/handle/inductive.ml         |  2 +-
 src/parsing/dkRule.ml           |  2 +-
 src/parsing/lpLexer.ml          |  2 +
 src/parsing/lpParser.ml         | 23 ++++++++---
 src/parsing/pretty.ml           |  6 ++-
 src/parsing/scope.ml            | 26 ++++++++----
 src/parsing/syntax.ml           | 28 +++++++++----
 src/tool/lcr.ml                 |  4 +-
 src/tool/tree_graphviz.ml       |  1 +
 tests/OK/cond_rules_st.lp       | 15 +++++++
 tests/export_dk.sh              |  2 +-
 tests/export_raw_dk.sh          |  2 +-
 24 files changed, 191 insertions(+), 50 deletions(-)
 create mode 100644 tests/OK/cond_rules_st.lp

diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf
index e3f0444ff..71c2efe43 100644
--- a/doc/lambdapi.bnf
+++ b/doc/lambdapi.bnf
@@ -33,7 +33,10 @@
 <constructor> ::= <uid> <param_list>* ":" <term>
 
 <rule> ::= <term> "↪" <term>
-         | <term> when <term> ≡ <term> "↪" <term>
+         | <term> when <condition> "↪" <term>
+
+<condition> ::= <term> ≡ <term>
+              | <term> «[<term>] <term>
 
 <unif_rule> ::= <equation> "↪" "[" <equation> (";" <equation>)* "]"
 
diff --git a/editors/emacs/lambdapi-smie.el b/editors/emacs/lambdapi-smie.el
index 6d42f46a6..c004074a2 100644
--- a/editors/emacs/lambdapi-smie.el
+++ b/editors/emacs/lambdapi-smie.el
@@ -144,7 +144,8 @@ Indent by `lambdapi-indent-basic' in proofs, and 0 otherwise."
       (indcons (args ":" sterm) ("|" args ":" sterm))
       (inddec (inddec "with" args ":" sterm "≔" indcons))
       (rules (rules "with" sterm "↪" sterm)
-             (rules "with" sterm "when" sterm "≡" sterm "↪" sterm))
+             (rules "with" sterm "when" condition "↪" sterm))
+      (condition (sterm "«[" sterm "]" sterm) (sterm "≡" sterm))
       (command
                ("begin" prfcontent "abort" ";")
                ("begin" prfcontent "admitted" ";")
@@ -242,7 +243,7 @@ The default lexer is used because the syntax is primarily made of sexps."
                       "print" "proofterm" "search" "type"))
      (lambdapi--query-indent))
 
-    (`(,_ . ,(or "," "↪" "→" "≡")) (smie-rule-separator kind))
+    (`(,_ . ,(or "«" "," "↪" "→" "≡")) (smie-rule-separator kind))
 
     (`(,(or :before :list-intro) . ,(or "≔" ":")) (smie-rule-separator kind))
     (`(:after . ,(or "≔" ":")) lambdapi-indent-basic)
diff --git a/editors/emacs/lambdapi-vars.el b/editors/emacs/lambdapi-vars.el
index 5271515d3..57513f00c 100644
--- a/editors/emacs/lambdapi-vars.el
+++ b/editors/emacs/lambdapi-vars.el
@@ -107,6 +107,7 @@
     (modify-syntax-entry ?→ "." table)
     (modify-syntax-entry ?↪ "." table)
     (modify-syntax-entry ?≔ "." table)
+    (modify-syntax-entry ?« "." table)
     (modify-syntax-entry ?$ "." table)
     (modify-syntax-entry ?? "." table)
     (modify-syntax-entry ?: "." table)
diff --git a/editors/vim/syntax/lambdapi.vim b/editors/vim/syntax/lambdapi.vim
index ebef338c9..5c1635815 100644
--- a/editors/vim/syntax/lambdapi.vim
+++ b/editors/vim/syntax/lambdapi.vim
@@ -209,6 +209,7 @@ syntax match Keyword ","
 syntax match Keyword ";"
 syntax match Keyword "_"
 syntax match Keyword "≡"
+syntax match Keyword "«"
 
 " Other special classes.
 syntax match Type "\u\w*"
@@ -217,6 +218,7 @@ syntax match PreProc  "?\(\<\h\w*\>\|\({|\([^|]\|\(|[^}]\)\)*|*|}\)\)"
 
 " Abbreviations.
 abbreviate --> ↪
+abbreviate << «
 abbreviate -> →
 abbreviate => ⇒
 abbreviate !  Π
diff --git a/misc/lambdapi.tex b/misc/lambdapi.tex
index 090e25789..7b4f739ad 100644
--- a/misc/lambdapi.tex
+++ b/misc/lambdapi.tex
@@ -26,6 +26,7 @@
   {≔}{$\coloneqq$}1
   {⊢}{$\vdash$}1
   {≡}{$\equiv$}1
+  {«}{$\ll$}1
   {𝔹}{$\mathbb{B}$}1
   {𝕃}{$\mathbb{L}$}1
   {ℕ}{$\mathbb{N}$}1
diff --git a/src/core/coercion.ml b/src/core/coercion.ml
index 8f9a7cffe..7cc708ecc 100644
--- a/src/core/coercion.ml
+++ b/src/core/coercion.ml
@@ -15,6 +15,6 @@ let _ =
     and t = mk_Patt (Some 1, "t", [||]) in
     let lhs = [a;a;t] and arities = [|0;0|] and names = [|"A";"t"|] in
     { lhs; names; rhs=t; arity=3; arities; vars_nb=2; xvars_nb = 0;
-      rule_pos = None; r_when = None }
+      rule_pos = None; r_when = R_None }
   in
   Sign.add_rule Ghost.sign (coerce, rule)
diff --git a/src/core/eval.ml b/src/core/eval.ml
index e154756e2..68ba96f52 100644
--- a/src/core/eval.ml
+++ b/src/core/eval.ml
@@ -357,6 +357,18 @@ and tree_walk : config -> sym -> stack -> (term * stack) option =
               let t1 = add_args (mk_Symb s1) v1 in
               let t2 = add_args (mk_Symb s2) v2 in
               if eq_modulo whnf cfg t1 t2 then ok else fail
+          | CondST((pth,op), p1, p2) ->
+              let v1 = vars.(fst p1) and v2 = vars.(fst p2) in
+              if Logger.log_enabled() then
+                log_rew "%aCondST(%s,%d,%d) : %a <<[%s] %a"
+                  D.depth !depth
+                  op (fst p1) (fst p2) Raw.term v1 op Raw.term v2;
+              let rec find (p: term -> bool) (t: term) =
+                match unfold t with
+                | Appl(Appl(Symb s,a1), a2)
+                     when s.sym_path=pth && s.sym_name=op -> p a1 || find p a2
+                | t -> p t in
+              if find (eq_modulo whnf cfg v1) v2 then ok else fail
           | CondFV(i,xs) ->
               let allowed =
                 (* Variables that are allowed in the term. *)
diff --git a/src/core/term.ml b/src/core/term.ml
index 76614350a..472a3f056 100644
--- a/src/core/term.ml
+++ b/src/core/term.ml
@@ -206,6 +206,14 @@ and sym =
 
 (** {3 Representation of rewriting rules} *)
 
+(** optional rule constraints *)
+and r_constraint =
+  (* equality constraint f p1 ... pn == g q1 ... qm *)
+  | R_EQ of (sym * int list) * (sym * int list)
+  (* subterm constraint p <<[op] q *)
+  | R_ST of sym * int * int
+  | R_None (* no constraint *)
+
 (** Representation of a rewriting rule. A rewriting rule is mainly formed of a
     LHS (left hand side),  which is the pattern that should be matched for the
     rule to apply, and a RHS (right hand side) giving the action to perform if
@@ -214,8 +222,7 @@ and sym =
   { lhs      : term list (** Left hand side (LHS). *)
   ; names    : string array (** Names of pattern variables. *)
   ; rhs      : term (** Right hand side (RHS). *)
-  ; r_when   : ((sym * int list) * (sym * int list)) option
-  (** conditional rule constraint. *)
+  ; r_when   : r_constraint (** conditional rule constraint. *)
   ; arity    : int (** Required number of arguments to be applicable. *)
   ; arities  : int array
   (** Arities of the pattern variables bound in the RHS. *)
diff --git a/src/core/term.mli b/src/core/term.mli
index 086e51abe..32bb0eb6e 100644
--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -138,6 +138,14 @@ and sym =
 
 (** {3 Representation of rewriting rules} *)
 
+(** optional rule constraints *)
+and r_constraint =
+  (* equality constraint f p1 ... pn == g q1 ... qm *)
+  | R_EQ of (sym * int list) * (sym * int list)
+  (* subterm constraint p <<[op] q *)
+  | R_ST of sym * int * int
+  | R_None (* no constraint *)
+
 (** Representation of a rewriting rule. A rewriting rule is mainly formed of a
     LHS (left hand side),  which is the pattern that should be matched for the
     rule to apply, and a RHS (right hand side) giving the action to perform if
@@ -146,8 +154,7 @@ and rule =
   { lhs      : term list (** Left hand side (LHS). *)
   ; names    : string array (** Names of pattern variables. *)
   ; rhs      : term (** Right hand side (RHS). *)
-  ; r_when   : ((sym * int list) * (sym * int list)) option
-  (** conditional rule constraint. *)
+  ; r_when   : r_constraint (** conditional rule constraint. *)
   ; arity    : int (** Required number of arguments to be applicable. *)
   ; arities  : int array
   (** Arities of the pattern variables bound in the RHS. *)
diff --git a/src/core/tree.ml b/src/core/tree.ml
index 7f768a3f3..e70f56729 100644
--- a/src/core/tree.ml
+++ b/src/core/tree.ml
@@ -78,6 +78,13 @@ module CP = struct
       let compare = Stdlib.compare
     end)
 
+  (** Functional sets of subterm constraints. *)
+  module STSet = Set.Make(
+    struct
+      type t = psym * pvar * pvar
+      let compare = Stdlib.compare
+    end)
+
   (** A pool of (convertibility and free variable) conditions. *)
   type t =
     { variables : pvar IntMap.t
@@ -95,6 +102,8 @@ module CP = struct
         stored at slot [i] in the [vars] array of [Eval.tree_walk]. *)
     ; eq_conds : TSet.t
     (** Set of pairs of terms that should be convertible. *)
+    ; st_conds : STSet.t
+    (** sets of subterm constraints. *)
     }
 
   (** [empty] is the condition pool holding no condition. *)
@@ -102,13 +111,15 @@ module CP = struct
     { variables = IntMap.empty
     ; nl_conds = PSet.empty
     ; fv_conds = IntMap.empty
-    ; eq_conds = TSet.empty }
+    ; eq_conds = TSet.empty
+    ; st_conds = STSet.empty }
 
   (** [is_empty pool] tells whether the pool of constraints is empty. *)
   let is_empty : t -> bool = fun pool ->
     PSet.is_empty pool.nl_conds
     && IntMap.is_empty pool.fv_conds
     && TSet.is_empty pool.eq_conds
+    && STSet.is_empty pool.st_conds
 
   (** [register_nl i (slot,vs) pool] registers the fact that the slot [slot]
       in the [vars] array correspond to a term stored at index [i] in the
@@ -140,6 +151,12 @@ module CP = struct
     let pv2 = List.map (fun i -> IntMap.find i pool.variables) a2 in
     { pool with eq_conds = TSet.add ((s1,pv1),(s2,pv2)) pool.eq_conds }
 
+  let register_st : psym -> int -> int -> t -> t =
+    fun op i j pool ->
+    let pv1 = IntMap.find i pool.variables in
+    let pv2 = IntMap.find j pool.variables in
+    { pool with st_conds = STSet.add (op, pv1, pv2) pool.st_conds }
+
   (** [constrained_nl i pool] tells whether index [i] in the RHS's environment
       has already been associated to a variable of the [vars] array. *)
   let constrained_nl : int -> t -> bool = fun slot pool ->
@@ -152,6 +169,7 @@ module CP = struct
     | CondNL(i,j) -> PSet.mem (i,j) pool.nl_conds
     | CondEQ(t1,t2) -> TSet.mem (t1,t2) pool.eq_conds
                        || TSet.mem (t2,t1) pool.eq_conds
+    | CondST(o,t1,t2) -> STSet.mem (o,t1,t2) pool.st_conds
     | CondFV(i,x) ->
         try Array.eq (=) x (IntMap.find i pool.fv_conds)
         with Not_found -> false
@@ -161,6 +179,8 @@ module CP = struct
     match cond with
     | CondNL(i,j)  -> {pool with nl_conds = PSet.remove (i,j) pool.nl_conds}
     | CondEQ(t,u) -> {pool with eq_conds = TSet.remove (t,u) pool.eq_conds}
+    | CondST(o,t,u) ->
+        {pool with st_conds = STSet.remove (o,t,u) pool.st_conds}
     | CondFV(i,xs) ->
         try
           let ys = IntMap.find i pool.fv_conds in
@@ -192,10 +212,20 @@ module CP = struct
       | p :: ps -> try Some(export (TSet.choose p.eq_conds))
                    with Not_found -> choose_eq ps
     in
+    let rec choose_st pools =
+      let export (op, t1, t2) = CondST(op,t1,t2) in
+      match pools with
+      | []      -> None
+      | p :: ps -> try Some(export (STSet.choose p.st_conds))
+                   with Not_found -> choose_st ps
+    in
     let res = choose_nl pools in
     if res = None then
       let res = choose_eq pools in
-      if res = None then choose_vf pools else res
+      if res = None then 
+        let res = choose_st pools in
+        if res = None then choose_vf pools else res
+      else res
     else res
 end
 
@@ -252,14 +282,23 @@ module CM = struct
       [0] index is used when going under abstractions. In that case, the field
       [arg_rank] is incremented. *)
 
+  (** rule constraints *)
+  type c_constraint =
+    | C_EQ of (psym * int list) * (psym * int list)
+    (** convertibility between flat terms *)
+    | C_ST of psym * int * int
+    (** subterm constraint between pattern variables *)
+    | C_None
+    (** no cnostraint *)
+
   (** A clause matrix row (schematically {i c_lhs ↪ c_rhs if cond_pool}). *)
   type clause =
     { c_lhs       : term array
     (** Left hand side of a rule. *)
     ; c_rhs       : rule
     (** Right hand side of a rule, and number of extra variables. *)
-    ; c_when      : ((psym * int list) * (psym * int list)) option
-    (** convertibility constraint for conditional rules *)
+    ; c_when      : c_constraint
+    (** constraints for conditional rules *)
     ; c_subst     : rhs_substit
     (** Substitution of RHS variables. *)
     ; xvars_nb    : int
@@ -329,10 +368,12 @@ module CM = struct
     let r2r ({lhs; xvars_nb; r_when; _} as c_rhs) =
       let c_lhs = Array.of_list lhs in
       let c_when = match r_when with
-        | None -> None
-        | Some ((s1,a1),(s2,a2)) ->
-            Some (((s1.sym_path,s1.sym_name), a1),
-                  ((s2.sym_path,s2.sym_name), a2)) in
+        | R_None -> C_None
+        | R_EQ ((s1,a1),(s2,a2)) ->
+            C_EQ (((s1.sym_path,s1.sym_name), a1),
+                  ((s2.sym_path,s2.sym_name), a2)) 
+        | R_ST (op,p,q) -> C_ST ((op.sym_path,op.sym_name), p, q)
+      in
       { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb; c_when }
     in
     let size = (* Get length of longest rule *)
@@ -425,7 +466,7 @@ module CM = struct
       in
       Array.for_all2 check lhs de && nonl lhs
     in
-    c_when = None && CP.is_empty cond_pool && (lhs = [||] || ripe lhs)
+    c_when = C_None && CP.is_empty cond_pool && (lhs = [||] || ripe lhs)
 
   (** [yield m] returns the next operation to carry out on matrix [m], that
       is, either specialising, solving a constraint or rewriting to a rule. *)
@@ -526,8 +567,15 @@ module CM = struct
         let c_when, cond_pool =
           let vars = cond_pool.variables in
           match r.c_rhs.r_when with
-          | None -> r.c_when, cond_pool
-          | Some ((op1,a1), (op2,a2)) when
+          | R_None -> r.c_when, cond_pool
+          | R_ST (sy, i, j) when 
+                 IntMap.mem i vars && IntMap.mem j vars ->
+              if Logger.log_enabled () then
+                log "Registering subterm constraint on position [%a] \
+                     %d <<[%s] %d"
+                  arg_path a.arg_path i sy.sym_name j;
+              C_None, CP.register_st (sy.sym_path,sy.sym_name) i j cond_pool
+          | R_EQ ((op1,a1), (op2,a2)) when
                  List.for_all (fun i -> IntMap.mem i vars) a1
                  && List.for_all (fun i -> IntMap.mem i vars) a2 ->
               if Logger.log_enabled () then
@@ -536,7 +584,7 @@ module CM = struct
                   arg_path a.arg_path
                   op1.sym_name (List.pp int " ") a1
                   op2.sym_name (List.pp int " ") a2;
-              None, CP.register_eq
+              C_None, CP.register_eq
                       ((op1.sym_path,op1.sym_name), a1)
                       ((op2.sym_path,op2.sym_name), a2)
                       cond_pool
diff --git a/src/core/tree_type.ml b/src/core/tree_type.ml
index 127d69d1e..89933a92f 100644
--- a/src/core/tree_type.ml
+++ b/src/core/tree_type.ml
@@ -59,6 +59,9 @@ type tree_cond =
       checking) of the term at the given index in the array? *)
   | CondEQ of (psym * pvar list) * (psym * pvar list)
   (** user rule condition: are the two terms equivalent *)
+  | CondST of psym * pvar * pvar
+  (** user rule condition: is the 1st pvar a subterm of the 2nd while
+   traversing psym calls *)
 
 (** {b NOTE} that when performing a [tree_cond.CondFV] check, we
     are concerned about variables that were bound in the term being reduced
@@ -76,6 +79,7 @@ let tree_cond : tree_cond pp = fun ppf tc ->
       out ppf "Eq(%s(%a),%s(%a))"
         (snd s1) (List.pp int ",") (List.map fst a1)
         (snd s2) (List.pp int ",") (List.map fst a2)
+  | CondST(op,p,q) -> out ppf "St(%s,%d,%d)" (snd op) (fst p) (fst q)
 
 (** Substitution of variables in a RHS. During the filtering process, some
     subterms of the filtered term may be stored in an array. Let [v] be that
diff --git a/src/export/rawdk.ml b/src/export/rawdk.ml
index 42f94fb8d..d39d350dd 100644
--- a/src/export/rawdk.ml
+++ b/src/export/rawdk.ml
@@ -136,7 +136,7 @@ let rec remove_wraps ({elt;_} as t) =
 let rule : p_rule pp =
   let varset ppf set = List.pp string ", " ppf (StrSet.elements set) in
   fun ppf {elt=(l,r,w);_} ->
-  if w = None then
+  if w = P_None then
     out ppf "[%a] %a --> %a.@."
       varset (pvars_lhs l) term (remove_wraps l) term r
   else
diff --git a/src/handle/inductive.ml b/src/handle/inductive.ml
index 3e6d2beb2..57c15b97f 100644
--- a/src/handle/inductive.ml
+++ b/src/handle/inductive.ml
@@ -347,7 +347,7 @@ let iter_rec_rules :
     let nonrec_dom _ _ next = next in
     let codom xs rhs _ ts =
       let cons_arg = P.appl_list (P.iden cons_sym.sym_name) (List.rev xs) in
-      Pos.make rules_pos (arec ind_sym ts cons_arg, rhs, None)
+      Pos.make rules_pos (arec ind_sym ts cons_arg, rhs, P_None)
     in
     fold_cons_type pos ind_pred_map "" ind_sym vs cons_sym inj_var
       init aux acc_rec_dom rec_dom acc_nonrec_dom nonrec_dom codom
diff --git a/src/parsing/dkRule.ml b/src/parsing/dkRule.ml
index 65e78eb3f..135420c42 100644
--- a/src/parsing/dkRule.ml
+++ b/src/parsing/dkRule.ml
@@ -155,4 +155,4 @@ let to_p_rule : p_dk_rule -> p_rule = fun r ->
   (* NOTE the computation order is important for setting arities properly. *)
   let lhs = build [] lhs in
   let rhs = build [] rhs in
-  Pos.make r.pos (lhs, rhs, None)
+  Pos.make r.pos (lhs, rhs, P_None)
diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml
index 20ce558e8..2e6efa99a 100644
--- a/src/parsing/lpLexer.ml
+++ b/src/parsing/lpLexer.ml
@@ -129,6 +129,7 @@ type token =
   | R_PAREN
   | R_SQ_BRACKET
   | SEMICOLON
+  | SUBTERM
   | THICKARROW (* only in Rocq *)
   | TURNSTILE
   | UNDERSCORE
@@ -332,6 +333,7 @@ let rec token ~allow_rocq_syntax lb =
   | ')' -> R_PAREN
   | ']' -> R_SQ_BRACKET
   | ';' -> SEMICOLON
+  | 0xab (* « *) -> SUBTERM
   | 0x22a2 (* ⊢ *) -> TURNSTILE
   | '|' -> VBAR
   | '_' -> UNDERSCORE
diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml
index b524f207e..3f464da8a 100644
--- a/src/parsing/lpParser.ml
+++ b/src/parsing/lpParser.ml
@@ -99,6 +99,7 @@ let string_of_token = function
   | SIMPLIFY -> "simplify"
   | SOLVE -> "solve"
   | STRINGLIT _ -> "string literal"
+  | SUBTERM -> "«"
   | SWITCH false -> "off"
   | SWITCH true -> "on or off"
   | SYMBOL -> "symbol"
@@ -533,7 +534,7 @@ let rec command pos1 (p_sym_mod:p_modifier list) (lb:'token lexbuf) :
       let (en, es) = List.(hd es, tl es) in
       let cat e es = P.appl (P.appl cons e) es in
       let rhs = List.fold_right cat es en in
-      let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs, None) in
+      let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs, P_None) in
       extend_pos lb (*__FUNCTION__*) pos1 (P_unif_rule(r))
   | COERCE_RULE ->
       if p_sym_mod <> [] then expected lb "" [SYMBOL]; (*or modifiers*)
@@ -689,7 +690,7 @@ and notation (lb:'token lexbuf): string Term.notation =
       expected lb "" [INFIX;POSTFIX;PREFIX;QUANTIFIER]
 
 and rule (lb:'token lexbuf):
-      (p_term * p_term * (p_term * p_term) option) loc =
+      (p_term * p_term * p_constraint) loc =
   if log_enabled() then log "%s" __FUNCTION__;
   let pos1 = current_pos lb in
   let l = term lb in
@@ -697,11 +698,21 @@ and rule (lb:'token lexbuf):
     if (current_token lb == WHEN) then begin
         consume WHEN lb;
         let t1 = term lb in
-        consume EQUIV lb;
-        let t2 = term lb in
-        Some (t1,t2)
+        if (current_token lb == EQUIV) then begin
+            consume EQUIV lb;
+            let t2 = term lb in
+            P_EQ(t1, t2)
+          end
+        else begin
+            consume SUBTERM lb;
+            consume L_SQ_BRACKET lb;
+            let op = term lb in
+            consume R_SQ_BRACKET lb;
+            let t2 = term lb in
+            P_ST (op,t1,t2)
+          end
       end
-    else None in
+    else P_None in
   consume HOOK_ARROW lb;
   let r = term lb in
   extend_pos lb (*__FUNCTION__*) pos1 (l, r, w)
diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml
index c05355899..299a57edf 100644
--- a/src/parsing/pretty.ml
+++ b/src/parsing/pretty.ml
@@ -189,9 +189,11 @@ and typ : p_term option pp = fun ppf t ->
 
 let rule : string -> p_rule pp = fun kw ppf {elt=(l,r,w);_} ->
   match w with
-  | None -> out ppf "%s %a ↪ %a" kw term l term r
-  | Some (t1,t2) -> out ppf "%s %a when %a ≡ %a ↪ %a"
+  | P_None -> out ppf "%s %a ↪ %a" kw term l term r
+  | P_EQ (t1,t2) -> out ppf "%s %a when %a ≡ %a ↪ %a"
                       kw term l term t1 term t2 term r
+  | P_ST (o,t1,t2) -> out ppf "%s %a when %a «[%a] %a ↪ %a"
+                      kw term l term t1 term o term t2 term r
 
 let inductive : string -> p_inductive pp =
   let cons ppf (id,a) = out ppf "@,| %a : %a" ident id term a in
diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
index f94c1a6ae..003d93af9 100644
--- a/src/parsing/scope.ml
+++ b/src/parsing/scope.ml
@@ -556,8 +556,11 @@ let scope_rule :
      arity. *)
   let pvs_when =
     match p_when with
-    | None -> []
-    | Some (t1,t2) ->
+    | P_None -> []
+    | P_EQ (t1,t2) ->
+        let (p1,_) = patt_vars t1 and (p2,_) = patt_vars t2 in
+        p1 @ p2
+    | P_ST (_o,t1,t2) ->
         let (p1,_) = patt_vars t1 and (p2,_) = patt_vars t2 in
         p1 @ p2 in
   let check_arity (m,i) =
@@ -631,19 +634,26 @@ let scope_rule :
   let arity = List.length lhs in
   let f i = try Hashtbl.find names i with Not_found -> string_of_int i in
   let names = Array.init vars_nb f in
+  let asPatt t = match unfold t with
+    | Patt (Some i, _, [||]) -> i
+    | _ -> fatal rule_pos "arguments should be patterns in condition [%a]."
+             term t in
+  let asSymb t = 
+    match unfold t with
+    | Symb s -> s
+    | _ -> fatal rule_pos "symbol expected [%a]." term t in
+  let p_asPatt t = asPatt (scope ~find_sym 0 mode ss Env.empty t) in
+  let p_asSymb t = asSymb (scope ~find_sym 0 mode ss Env.empty t) in
   let pw2rw t =
-    let asPatt t = match unfold t with
-      | Patt (Some i, _, [||]) -> i
-      | _ -> fatal rule_pos "arguments should be patterns in condition [%a]."
-               term t in
     let t = scope ~find_sym 0 mode ss Env.empty t in
     match get_args t with
       Symb s, args ->  (s, List.map asPatt args)
     | _ -> fatal rule_pos "function should be a global symbol in [%a]." term t
   in
   let r_when = match p_when with
-    | None -> None
-    | Some (t1,t2) -> Some (pw2rw t1, pw2rw t2) in
+    | P_None -> R_None
+    | P_EQ (t1,t2) -> R_EQ (pw2rw t1, pw2rw t2)
+    | P_ST (o,t1,t2) -> R_ST (p_asSymb o, p_asPatt t1, p_asPatt t2) in
   let r = {lhs; names; rhs; arity; arities; vars_nb; xvars_nb;
            rule_pos; r_when} in
   (sym,r)
diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml
index ae159fd14..356ad8fdc 100644
--- a/src/parsing/syntax.ml
+++ b/src/parsing/syntax.ml
@@ -133,8 +133,13 @@ let rec pvars_lhs : p_term -> StrSet.t = fun {elt;pos} ->
   | P_Expl u
     -> pvars_lhs u
 
+type p_constraint =
+  P_EQ of p_term * p_term           (* t1 == t2 *)
+| P_ST of p_term * p_term * p_term  (* t2 <<[t1] t3 *)
+| P_None
+
 (** Parser-level rewriting rule representation. *)
-type p_rule_aux = p_term * p_term * (p_term * p_term) option
+type p_rule_aux = p_term * p_term * p_constraint
 type p_rule = p_rule_aux loc
 
 (** Parser-level inductive type representation. *)
@@ -182,7 +187,7 @@ module P  = struct
   let abst_list : p_ident option list -> p_term -> p_term = fun idopts t ->
     List.fold_right abst idopts t
 
-  let rule : p_term -> p_term -> (p_term * p_term) option -> p_rule =
+  let rule : p_term -> p_term -> p_constraint -> p_rule =
     fun l r w -> Pos.none (l,r,w)
 end
 
@@ -404,13 +409,21 @@ and eq_p_params : p_params eq = fun (i1,ao1,b1) (i2,ao2,b2) ->
   List.eq (Option.eq eq_p_ident) i1 i2
   && Option.eq eq_p_term ao1 ao2 && b1 = b2
 
+let eq_p_constraint: p_constraint eq = fun c1 c2 ->
+  match c1,c2 with
+    P_EQ (t1,u1), P_EQ (t2,u2) -> eq_p_term t1 t2 && eq_p_term u1 u2
+  | P_ST (o1,t1,u1), P_ST (o2,t2,u2) -> 
+      eq_p_term o1 o2 && eq_p_term t1 t2 && eq_p_term u1 u2
+  | P_None, P_None -> true
+  | _ -> false
+
 let pair_eq: 'a eq -> 'b eq -> ('a * 'b) eq = fun eq1 eq2 (x1,y1) (x2,y2) ->
   eq1 x1 x2 && eq2 y1 y2
 
 let eq_p_rule : p_rule eq = fun {elt=(l1,r1,w1);_} {elt=(l2,r2,w2);_} ->
   eq_p_term l1 l2
   && eq_p_term r1 r2
-  && Option.eq (pair_eq eq_p_term eq_p_term) w1 w2
+  && eq_p_constraint w1 w2
 
 let eq_p_inductive : p_inductive eq =
   let eq_cons (i1,t1) (i2,t2) = eq_p_ident i1 i2 && eq_p_term t1 t2 in
@@ -624,14 +637,15 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a =
 
   let fold_term : 'a -> p_term -> 'a = fold_term_vars StrSet.empty in
 
-  let fold_when : 'a -> (p_term * p_term) option -> 'a = fun a w ->
+  let fold_constraint : 'a -> p_constraint -> 'a = fun a w ->
     match w with
-    | Some (t1,t2) -> fold_term (fold_term a t1) t2
-    | None -> a
+    | P_EQ (t1,t2) -> fold_term (fold_term a t1) t2
+    | P_ST (o,t1,t2) -> fold_term (fold_term (fold_term a o) t1) t2
+    | P_None -> a
   in
 
   let fold_rule : 'a -> p_rule -> 'a = fun a {elt=(l,r,w);_} ->
-    fold_when (fold_term (fold_term a l) r) w
+    fold_constraint (fold_term (fold_term a l) r) w
   in
 
   let fold_rwpatt_vars : StrSet.t -> 'a -> p_rwpatt -> 'a = fun vs a p ->
diff --git a/src/tool/lcr.ml b/src/tool/lcr.ml
index d70323b97..ef2b81f35 100644
--- a/src/tool/lcr.ml
+++ b/src/tool/lcr.ml
@@ -55,7 +55,7 @@ let is_definable : sym -> bool = fun s ->
 (** [rule_of_def s d] creates the rule [s --> d]. *)
 let rule_of_def : sym -> term -> rule = fun s rhs ->
   {lhs=[]; names=[||]; rhs; arity=0; arities=[||]; vars_nb=0; xvars_nb=0;
-   rule_pos=s.sym_pos; r_when = None}
+   rule_pos=s.sym_pos; r_when = R_None}
 
 (** [replace t p u] replaces the subterm of [t] at position [p] by [u]. *)
 let replace : term -> subterm_pos -> term -> term = fun t p u ->
@@ -457,7 +457,7 @@ let typability_constraints : Pos.popt -> term -> subs option = fun pos t ->
     match get_args_len l with
     | Symb s, lhs, arity ->
       let r = {lhs; names=[||]; rhs; arity; arities=[||]; vars_nb=0;
-               xvars_nb=0; rule_pos=Some(new_rule_id()); r_when = None} in
+               xvars_nb=0; rule_pos=Some(new_rule_id()); r_when = R_None} in
       Some (s,r)
     | _ -> None
   in
diff --git a/src/tool/tree_graphviz.ml b/src/tool/tree_graphviz.ml
index 4af09c70c..2780eb305 100644
--- a/src/tool/tree_graphviz.ml
+++ b/src/tool/tree_graphviz.ml
@@ -46,6 +46,7 @@ let tree_to_dot : Format.formatter -> _ dtree -> unit = fun ppf dtree ->
       | CondNL((i,vi), (j,vj)) ->
           out ppf "%d[%a] ≡ %d[%a]" i ar vi j ar vj
       | CondFV(i,vs) -> out ppf "%a ⊆ FV(%d)" ar vs i
+      | CondST(op,i,j) -> out ppf "%d «[%s] %d" (fst i) (snd op) (fst j)
       | CondEQ(((_p1,s1),a1), ((_p2,s2),a2)) ->
           out ppf "%s[%a] ≡ %s[%a]"
             s1 (List.pp int ",") (List.map fst a1)
diff --git a/tests/OK/cond_rules_st.lp b/tests/OK/cond_rules_st.lp
new file mode 100644
index 000000000..9a8d98fcd
--- /dev/null
+++ b/tests/OK/cond_rules_st.lp
@@ -0,0 +1,15 @@
+symbol Prop: TYPE;
+symbol ∧: Prop → Prop → Prop;
+notation ∧ infix right 7;
+constant symbol ⊤ : Prop;
+constant symbol ⊥ : Prop;
+
+sequential symbol doubles_in_and : Prop → Prop;
+
+rule doubles_in_and ($p ∧ $q) when $p «[@∧] $q ↪ ⊤
+with doubles_in_and ($p ∧ $q) ↪ doubles_in_and $q
+with doubles_in_and $p ↪ ⊥;
+
+
+assert p q r ⊢ doubles_in_and (p ∧ q ∧ r) ≡ ⊥;
+assert p q r ⊢ doubles_in_and (q ∧ p ∧ r ∧ p) ≡ ⊤;
diff --git a/tests/export_dk.sh b/tests/export_dk.sh
index e30ed6590..d53991647 100755
--- a/tests/export_dk.sh
+++ b/tests/export_dk.sh
@@ -50,7 +50,7 @@ do
         # use Tactic
         first_hyp|all_hyps);;
         # use cond rules
-        cond_rules);;
+        cond_rules*);;
         # requires an excluded file
         assume|first_hyp);;
         # default case
diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh
index 40965bfdf..fd01bc2bf 100755
--- a/tests/export_raw_dk.sh
+++ b/tests/export_raw_dk.sh
@@ -59,7 +59,7 @@ do
         # module alias
         alias);;
         # conditional rules
-        cond_rules);;
+        cond_rules*);;
         # proofs
         why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp|all_hyps);;
         # "open"

From 634c3d4b2ed50ccc3b6e900c817e301cf31cef20 Mon Sep 17 00:00:00 2001
From: bodeveix <bodeveix@irit.fr>
Date: Tue, 7 Jul 2026 16:18:09 +0200
Subject: [PATCH 09/10] sanity checks

---
 src/core/tree.ml      | 6 +++---
 src/parsing/scope.ml  | 2 +-
 src/parsing/syntax.ml | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/core/tree.ml b/src/core/tree.ml
index e70f56729..e1c12d7a7 100644
--- a/src/core/tree.ml
+++ b/src/core/tree.ml
@@ -222,7 +222,7 @@ module CP = struct
     let res = choose_nl pools in
     if res = None then
       let res = choose_eq pools in
-      if res = None then 
+      if res = None then
         let res = choose_st pools in
         if res = None then choose_vf pools else res
       else res
@@ -371,7 +371,7 @@ module CM = struct
         | R_None -> C_None
         | R_EQ ((s1,a1),(s2,a2)) ->
             C_EQ (((s1.sym_path,s1.sym_name), a1),
-                  ((s2.sym_path,s2.sym_name), a2)) 
+                  ((s2.sym_path,s2.sym_name), a2))
         | R_ST (op,p,q) -> C_ST ((op.sym_path,op.sym_name), p, q)
       in
       { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb; c_when }
@@ -568,7 +568,7 @@ module CM = struct
           let vars = cond_pool.variables in
           match r.c_rhs.r_when with
           | R_None -> r.c_when, cond_pool
-          | R_ST (sy, i, j) when 
+          | R_ST (sy, i, j) when
                  IntMap.mem i vars && IntMap.mem j vars ->
               if Logger.log_enabled () then
                 log "Registering subterm constraint on position [%a] \
diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
index 003d93af9..48fdd2e81 100644
--- a/src/parsing/scope.ml
+++ b/src/parsing/scope.ml
@@ -638,7 +638,7 @@ let scope_rule :
     | Patt (Some i, _, [||]) -> i
     | _ -> fatal rule_pos "arguments should be patterns in condition [%a]."
              term t in
-  let asSymb t = 
+  let asSymb t =
     match unfold t with
     | Symb s -> s
     | _ -> fatal rule_pos "symbol expected [%a]." term t in
diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml
index 356ad8fdc..9b7a4caeb 100644
--- a/src/parsing/syntax.ml
+++ b/src/parsing/syntax.ml
@@ -412,7 +412,7 @@ and eq_p_params : p_params eq = fun (i1,ao1,b1) (i2,ao2,b2) ->
 let eq_p_constraint: p_constraint eq = fun c1 c2 ->
   match c1,c2 with
     P_EQ (t1,u1), P_EQ (t2,u2) -> eq_p_term t1 t2 && eq_p_term u1 u2
-  | P_ST (o1,t1,u1), P_ST (o2,t2,u2) -> 
+  | P_ST (o1,t1,u1), P_ST (o2,t2,u2) ->
       eq_p_term o1 o2 && eq_p_term t1 t2 && eq_p_term u1 u2
   | P_None, P_None -> true
   | _ -> false

From 1a3435281809041de94cdd455c5ab619a020a7f5 Mon Sep 17 00:00:00 2001
From: bodeveix <bodeveix@irit.fr>
Date: Thu, 9 Jul 2026 15:08:25 +0200
Subject: [PATCH 10/10] merge-master

---
 src/parsing/lpParser.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml
index e5e720957..c48ccaa80 100644
--- a/src/parsing/lpParser.ml
+++ b/src/parsing/lpParser.ml
@@ -599,7 +599,7 @@ and command (lb:'token lexbuf) : p_command =
         let (en, es) = List.(hd es, tl es) in
         let cat e es = P.appl (P.appl cons e) es in
         let rhs = List.fold_right cat es en in
-        let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs) in
+        let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs, P_None) in
         extend_pos lb (*__FUNCTION__*) pos1 (P_unif_rule(r))
     | COERCE_RULE ->
         consume_token lb;