Based on the one of Ralf Jung for Iris.

Some were already maximally implicit, some were not. Now it is consistent.

update build system and README

See merge request !1

It no longer requires the functions on both sides of the relation
to be syntactically the same.

This fixes issue #65.

This approach is originally by Robbert

Fix fixes issue #63.

Rename:

- prefix_of -> prefix and suffix_of -> suffix because that saves keystrokes
  in lemma names. However, keep the infix notations with l1 `prefix_of` l2 and
  l1 `suffix_of` l2 because those are easier to read.
- change the notation l1 `sublist` l2 into l1 `sublist_of` l2 to be consistent.
- rename contains -> submseteq and use the notation ⊆+

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing

Also make names more consistent.

We typically use the _1 and _2 suffix to denote individual directions
of a lemmas that is a biimplication.

case H; clear H would fail when H is dependent whereas destruct H
would succeed on that, but just not clear it.