let f a =
(* L.warn (Printf.sprintf "Convertible: %b" a); *)
if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt)
else error3 err c xv vv w
in
ZR.are_convertible f st c w vv
let f a =
(* L.warn (Printf.sprintf "Convertible: %b" a); *)
if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt)
else error3 err c xv vv w
in
ZR.are_convertible f st c w vv