contradiction tactic

Stream: new members

[Sarah]

My strategy was to close the proof goal by using a contradiction proof. I have two contradicting hypotheses but somehow the contradiction tactic doesn't kick in. I doubled checked the types etc. so the hypothesis are exactly contradictory. Can somehow explain why the contradiction tactic doesn't close it ? And is there another strategy to then derive the contradiction ?
iT and h3 are contradictory
image.png

[Edward van de Meent]

i think omega might solve this?

[Aaron Liu]

contradiction only solves "simple" contradictions, apparently this was not a "simple" contradiction.

[Edward van de Meent]

other than that, exact (not_le_of_lt iT h3).elim might work