- fo_unif_subst subst context metasenv newhety expty ugraph in
- Some ((newt,newty), subst, metasenv, ugraph)
+ fo_unif_subst subst context metasenv newhety expty ugraph
+ in
+ let b, ugraph =
+ CicReduction.are_convertible
+ ~subst ~metasenv context infty expty ugraph
+ in
+ if b then
+ Some ((t,infty), subst, metasenv, ugraph)
+ else
+ let newt = unvariant newt in
+ Some ((newt,newty), subst, metasenv, ugraph)