+ let fo_unif_subst =
+ let (lower,upper) =
+ match t1,t2 with
+ C.Meta (n,_), C.Meta (m,_) when n < m ->
+ (fun t1 t2 -> t1), (fun t1 t2 -> t2)
+ | _, C.Meta _ ->
+ (fun t1 t2 -> t1), (fun t1 t2 -> t2)
+ | _,_ ->
+ (fun t1 t2 -> t2), (fun t1 t2 -> t1)
+ in
+ fun subst context metasenv m1 m2 ->
+ fo_unif_subst subst context metasenv (lower m1 m2) (upper m1 m2)
+ in