explicitly referencing case rule as per http://stackoverflow.com/questions/18686865/how-can-i-bind-the-schematic-variable-case-in-a-rule-for-proof-by-cases#comment27537885_18690462
new inference rule Union_member
more progress in theorem injections_equiv; introducing lemma injections_paste