let max_real_symm = prove_by_refinement( `!a b. max_real a b = max_real b a`, [ REP_GEN_TAC; REWRITE_TAC[max_real]; COND_CASES_TAC; USE 0 (MATCH_MP (REAL_ARITH `a < b ==> ~(b < a)`)); ASM_REWRITE_TAC[]; COND_CASES_TAC; ASM_REWRITE_TAC[]; UND 0; UND 1; REAL_ARITH_TAC; ]);; let SIGMAHAT_EQ = prove( `!x1 x2 x3 x4 x5 x6. sigmahat_x x1 x2 x3 x4 x5 x6 = sigmahat_x' x1 x2 x3 x4 x5 x6`, REPEAT STRIP_TAC THEN REWRITE_TAC [sigmahat_x';sigmahat_x] THEN LET_TAC THEN LET_TAC THEN LET_TAC THEN LET_TAC THEN LET_TAC THEN LET_TAC THEN LET_TAC THEN LET_TAC THEN LET_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[] LET_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN LET_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN LET_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN LET_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN LET_TAC THEN REWRITE_ALL_TAC[] ONCE_REWRITE_TAC[MAX_REAL_SYMM] let TEST = prove(`!x:bool. x = x`, STRIP_TAC THEN REWRITE_TAC []);; (program-get-line) let x = 5 e (REPEAT STRIP_TAC) e (REWRITE_TAC[sigmahat_sean_x;sigmahat_x;LET_DEF;LET_END_DEF]) e (REPEAT COND_CASES_TAC THEN REWRITE_TAC[]) e (MESON_TAC[])