Project contains a bunch of "admit" commands

[anton-trunov]

We should get rid of those.

[anton-trunov]

Partially solved by #13

[palmskog]

The only admitted lemma that's not an Example (and therefore seemingly not necessary to Qed) is the following in noaliasBT.v:

Lemma noaliasR2 s x y (f : Scan.form s) (g : NoAlias2.form x y s) :
               def f -> NoAlias2.eq_of g.
Proof. admit. Admitted.

To me, this lemma doesn't look provable, and its only use is in throwaway examples. @anton-trunov does it look provable to you?

[anton-trunov]

does it look provable to you?

It is provable, please see #17.

[anton-trunov]

Fixed by b9a21a0