(* on étend les substitutions en l'identité en dehors de leur domaine *)
let rec subst_tvar s x =  try List.assoc x s with Not_found -> Tvar x
(* on étend les aux termes *)
let rec subst_texp s = function 
    Tint -> Tint
  | Tvar x -> subst_tvar s x
  | Tarrow (t1, t2) -> Tarrow (subst_texp s t1, subst_texp s t2);;

(* exemple *)
let t = Tarrow (Tarrow (Tvar 1, Tvar 2), Tarrow (Tvar 1, Tvar 2))
let s = [ 1, Tint]
let t1 = subst_texp s t;;