Proved rule_start, which needed a ton of refactoring. ProtocolLogic introduced.
Fixed up the post-condition of the method-spec for start. Now all traces must equal 'end'.

Safety for start is now fully proven, which means start is too. Yay.
Yanked out traces. Yay.
Improved the marshall-predicate. It works much better now.
Redefined psasn to be an open, added pspec, and started work on IsMarshallable lemmas.
Switched from marshallable to decidable. Added list-predicate.
Cleaned out some admitted lemmas, and tagged some admits with usage.
Fixed an import after CaseStudies/List.v was added.
Maded existentialise_triple work with psasns.
Improved the Decidable lemmas, shortened the List-decideability lemmas, and added DecidableSasn.
Swapped the ordering in the List predicates so they are conforming to the norm.
Added missing DecidableSasn morphism.
Changed the axiomatic semantics to use DecidableSasn.
More work on the List case-study
Reverted back to the old method_spec that uses normal substitution, now that psasn supports that.
Proved more of the Axiomatic Semantics in the extended memory model.