     THEN0 (fs [] \\ fs [state_rel_def] \\ rveq \\ fs[])     \\ fs [option_case_eq,pair_case_eq] \\ rveq \\ fs []     \\ `state_rel (dec_clock s0) (dec_clock 0 t0)` by          fs [flatSemTheory.dec_clock_def,dec_clock_def,state_rel_def]     