Title: Proving correctness of constructor implementations