Improve terminal proof methods in output

The Isabelle simplifier apparently chokes on recursive message equations
derived in the proofs for the ASW and HiddenAgree protocols. This commit
heuristically fixes the issue by applying additional proof methods at
each terminal proof step.

Tested with all example protocols from the classic, spore, iso9798 sets.
Running times are not affected significantly.
Distinguish inequalities on type level
Add disjunction operator to property formulas

We use disjunction to model agreement with roles split due to branching
control flow.
Refine matching example protocols, use disjunction
Fix proof method for exploiting long term key secrecy

Required for the HiddenAgree protocol, proof checking did not terminate.
Tested with all example protocols from the classic, spore, iso9798 sets.