Fix to init definitions + further progress on metatheory changes from init scheme

Author: didriklundberg

hol/metatheory/p4_e_progressScript.sml

@@ -2172,7 +2172,7 @@ srw_tac [boolSimps.DNF_ss][] >>
 Cases_on `is_consts (MAP (λ(f_,e_,tau_,b_). (e_)) f_e_tau_b_list)` >| [
  (* starting from the left disjuction
    if all members are constsants then we know that
-   vl_of_el actually exsists *)
+   vl_of_el actually exists *)
 
  DISJ2_TAC >>
 
@@ -2263,7 +2263,7 @@ srw_tac [boolSimps.DNF_ss][] >>
 Cases_on `is_consts (MAP (λ(f_,e_,tau_,b_). (e_)) f_e_tau_b_list)` >| [
  (* starting from the left disjuction
    if all members are constsants then we know that
-   vl_of_el actually exsists *)
+   vl_of_el actually exists *)
 
  DISJ2_TAC >>
 

hol/metatheory/p4_e_subject_reductionScript.sml

@@ -83,7 +83,7 @@ QED
 
 
 (******   Subject Reduction for expression    ******)
-(*t_scopes_consistent is with respect to the expression's global, not the passed, because at that point we are comparing with respect to the passed scope that is already exsists in the expression *)
+(*t_scopes_consistent is with respect to the expression's global, not the passed, because at that point we are comparing with respect to the passed scope that is already exists in the expression *)
 
 val sr_exp_def = Define `
  sr_exp (e) (ty:'a itself) =
@@ -4108,7 +4108,7 @@ QED
 
 
 
-Theorem lookup_lval_exsists:
+Theorem lookup_lval_exists:
 ! ss v x s .
 lookup_lval (ss) (lval_field x s) = SOME v ==>
 ? v' . lookup_lval (ss) x = SOME v' 
@@ -4267,7 +4267,7 @@ gvs[] >| [
   `t_sl` , `b`, `d`])) >>
  gvs[] >>
 
- IMP_RES_TAC lookup_lval_exsists  >>
+ IMP_RES_TAC lookup_lval_exists  >>
  gvs[] >>
 
  (*

hol/metatheory/p4_frames_progressScript.sml

@@ -683,7 +683,7 @@ Cases_on ‘is_d_none_in h1’ >> gvs[] >| [
     IMP_RES_TAC v_types_ev >>
     FIRST_X_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL [‘pre_passed_tslg’, ‘pre_tsl’, ‘T_e’])) >>
 
-    (* since the lval is typed, and also the value is typed, then there exsists a scope such that  assign lval = v *)              
+    (* since the lval is typed, and also the value is typed, then there exists a scope such that  assign lval = v *)              
     ASSUME_TAC assignment_scope_exists >>  
     FIRST_X_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL [‘pre_local’,‘pre_gscope_passed’,‘pre_tsl’,‘pre_passed_tslg’,‘t’,‘F’,‘lval’,‘v’,‘T_e’])) >>
     gvs[] >>                
@@ -1135,7 +1135,7 @@ Cases_on ‘notret status'’ >| [
   CONV_TAC $ SWAP_EXISTS_CONV >>
   Q.EXISTS_TAC ‘scopest'’ >> gvs[] >>
 
- (* now we show that scopes to retrieve exsists & it's length is 2 *)
+ (* now we show that scopes to retrieve exists & it's length is 2 *)
  subgoal ‘LENGTH gscope' = 2 ’ >- ( IMP_RES_TAC type_scopes_list_LENGTH >> gvs[WT_c_cases] ) >>
 
   IMP_RES_TAC assign_star_length_2 >>