are_convertible f a c m1 w1 m2 w2
(* we detect the AUT-QE reduction rule for type/prop inclusion *)
| Sort_ _, Bind_ (l2, id2, w2, t2) when !nsi ->
let m1, m2 = inc m1, inc m2 in
let f c = are_convertible f a c m1 (term_of_whdr r1) m2 t2 in
are_convertible f a c m1 w1 m2 w2
(* we detect the AUT-QE reduction rule for type/prop inclusion *)
| Sort_ _, Bind_ (l2, id2, w2, t2) when !nsi ->
let m1, m2 = inc m1, inc m2 in
let f c = are_convertible f a c m1 (term_of_whdr r1) m2 t2 in