let rec can ((e, p) as s) a =
  let sigma f al = (sigma f al, Jst.dep0) in
  let interp_can f = 
    let i = Sym.theory_of f in
      Jst.Eqtrans.compose_partial1
        (E.find s i) 
        (can s)
  in 
    if Term.is_var a then
      Partition.find p a
    else 
      try
        Jst.Eqtrans.compose
          (E.inv s)                       
          (Jst.Eqtrans.mapargs sigma interp_can)
          a 
      with 
          Not_found ->
            Partition.find p a