op ORELSE_LT : list_tactic * list_tactic -> list_tactic
Applies first list-tactic, and if it fails, applies the second instead.
If ltac1 and ltac2 are list-tactics, ltac1 ORELSE_LT ltac2
is a list-tactic which applies ltac1 to a goal list, and if it fails,
applies ltac2 to the goals.
The application of ORELSE_LT to a pair of list-tactics never fails.
The resulting list-tactic fails if both ltac1 and ltac2 fail
when applied to the relevant goals.