let rec solve e =
  let (a, b, _) = Fact.d_equal e in
    solvel [(a, b)] []

and solvel el sl =
  match el with
    | [] -> sl
    | (a, b) :: el1 ->
        solve1 (a, b) el1 sl 

and solve1 (a, b) el sl = 
  if Term.eq a b then 
    solvel el sl
  else if Term.is_var b then
    solvevar (b, a) el sl
  else match a with
    | App(Coproduct(op), [x]) ->  

(** solve inY(x) = b is x = outY(b). *)


        let rhs' = match op with  

(** solve outY(x) = b is x = inY(b). *)


          | InL -> mk_outl b
          | InR -> mk_outr b
          | OutL -> mk_inl b
          | OutR -> mk_inr b
        in 
          solvel ((x, rhs') :: el) sl
    | _ -> 
        solvevar (a, b) el sl
        
and solvevar (x, b) el sl =
  if is_var b then
    solvel el (add (Term.orient (x, b)) sl)
  else if Term.occurs x b then
    raise Exc.Inconsistent
  else 
    solvel el (add (x, b) sl)

and add (a, b) sl =
  if Term.eq a b then  sl else
    let e = Fact.mk_equal a b None in  (* does not swap terms *)
      e :: (substl a b sl)             (* since [a] and [b] are oriented *)

and substl a b = 
  List.map 
    (fun e -> 
       let (x, y, _) = Fact.d_equal e in
         Fact.mk_equal x (subst1 y a b) None)

and subst1 a x b =      (* substitute [x] by [b] in [a]. *)
  map (fun y -> if Term.eq x y then b else y) a