- | (_, U.Negative, _)::tl ->
- find_matches metasenv context ugraph lift_amount term tl
- | (pos, U.Positive, (_, (_, _, _, o), _, _))::tl
- when (pos = Left && o = U.Lt) || (pos = Right && o = U.Gt) ->
- find_matches metasenv context ugraph lift_amount term tl
- | (pos, U.Positive, (proof, (ty, left, right, o), metas, args))::tl ->
+ | (pos, (proof, (ty, left, right, o), metas, args))::tl ->