+ | C.Meta (n,lc), C.Meta (m,lc') when
+ let _,_,tyn = NCicUtils.lookup_meta n metasenv in
+ let _,_,tym = NCicUtils.lookup_meta m metasenv in
+ let tyn = NCicSubstitution.subst_meta lc tyn in
+ let tym = NCicSubstitution.subst_meta lc tym in
+ match tyn,tym with
+ NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
+ NCicEnvironment.universe_lt u1 u2
+ | _,_ -> false ->
+ instantiate rdb test_eq_only metasenv subst context m lc'
+ (NCicReduction.head_beta_reduce ~subst t1) (not swap)