let rec fnd th s a  =
    if Th.eq th Th.u || Th.eq th Th.app then  
      a
    else if Th.is_fully_interp th then
      let b = find th s a in  (* Context.find *)
        b
    else 
      findequiv th s a
        
  and findequiv th s a =
    let choose s = V.choose (v_of s) in
      try
        choose s
          (fun x ->
             try Some(apply th s x) 
             with Not_found -> None)
          a
      with
          Not_found -> a