LARA

Example Verification Condition and Its Proof