Ordering is now: first by number of assumptions, second by the substitution size. Treat elim/dest rules like erule/drule would: * "elim" is now a subset of "dest" and matches on conclusion of goal and major premise against any premise of goal. Computed substitution size takes both into account. * "dest" no longer has a restriction that limits its conclusion to a var. (contributed by Raf)

addedd ID line