* Add proofs to make consistency checks with the geometry model