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[])