Try match an expression (e.g. ($x |-> ($x * $x)) is injective; ) to an expression model (e.g. $f is injective; ).

Expression to be matched

Expression model

Compare Expression