Infer from implication with variable condition correctly

[Charles-Johnson]

The transitivity of > can be expressed as

let ((_y_ exists_such_that) (_x_ > _y_) and _y_ > _z_) => _x_ > _z_

But if reductions of expressions containing variables are interpreted as meaning that the expression is true no matter what concepts are substituted for the variables, the same transitivity property can be expressed as

let ((_x_ > _y_) and _y_ > _z_) => _x_ > _z_

When evaluating 2 > 0, the expression is generalised to _x_ > _z_ which has sufficient conditions matching the pattern (_x_ > _y_) and _y_ and _z_. Substituting variables leads to 2 > 0 having sufficient conditions matching the pattern (2 > _y_) and _y_ > 0. At this point the ContextSearch::find_example can be used to find that (2 > 1) and 1 > 0 matches which implies 2 > 0.

The interpreter currently would only conclude that 2 > 0 if (2 > _y_) and _y_ > 0 for all _y_ which is clearly not desired.

[Charles-Johnson]

currently

let _x_ -> _y_

gives no error message. It should under the new proposed interpretation because it would mean any reduction is true which cannot hold because a -> b and b -> a would be true, causing an infinite evaluation cycle.

[Charles-Johnson]

It may be possible now to express transitivity without exists_such_that. I need to test this