Started sketching inference completeness

There is a statement of a theorem, but I think that the invariants are
not right, yet.