let is_equal s x y = 
  assert(Term.is_var x);
  assert(Term.is_var y);
  let (x', rho) = find s x         (* [rho |- x = x'] *)
  and (y', tau) = find s y in 
    if Term.eq x' y' then          (* [tau |- y = y'] *)
      Some(Jst.dep2 rho tau)
    else 
      None