let well_formed_subst sigma =
try
ignore (
List.fold_left (fun (acc_x, acc_y) (x, y) ->
if Hstring.list_mem x acc_x || Hstring.list_mem y acc_y
then raise Exit;
x :: acc_x, y :: acc_y
) ([],[]) sigma);
true
with Exit -> false