Remove the loop axiom

The axiom was loop : forall A, Obj A and used as the base case of
selection. The new version of selection takes a proof of l in dom A.

The init function of type forall A, Obj A is implemented.