| (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Def (b2,t2))::cl2 ->
if n1 = n2 &&
NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 &&
NCicReduction.are_convertible ctx ~subst ~metasenv b1 b2 then
| (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Def (b2,t2))::cl2 ->
if n1 = n2 &&
NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 &&
NCicReduction.are_convertible ctx ~subst ~metasenv b1 b2 then