Put forward_simulation and backward_simulation in Prop instead of Type

The original presentation of forward_simulation and backward_simulation diagrams was using records containing types, relations, and properties over these.  These records had to live in Type because in Prop the projections could not be defined.

This was causing problems with proofs of statements such as

     (exists x, P x) -> forward_simulation sem1 sem2

because the exists could not be eliminated in a Type context.

This commit re-expresses the simulation diagrams as a record of properties (in Prop) and an inductive (in Prop too) that packs the record with the types and relations.  The external interface of module Smallstep is unchanged, it's only the proofs in Smallstep and Behaviors that take a slightly different shape.

1 files changed, 275 insertions, 255 deletions

diff --git a/common/Smallstep.v b/common/Smallstep.v
index 71cef35f..9c91243a 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -513,43 +513,49 @@ Open Scope smallstep_scope.
 
 (** The general form of a forward simulation. *)
 
-Record forward_simulation (L1 L2: semantics) : Type :=
-  Forward_simulation {
-    fsim_index: Type;
-    fsim_order: fsim_index -> fsim_index -> Prop;
-    fsim_order_wf: well_founded fsim_order;
-    fsim_match_states :> fsim_index -> state L1 -> state L2 -> Prop;
+Record fsim_properties (L1 L2: semantics) (index: Type)
+                       (order: index -> index -> Prop)
+                       (match_states: index -> state L1 -> state L2 -> Prop) : Prop := {
+    fsim_order_wf: well_founded order;
     fsim_match_initial_states:
       forall s1, initial_state L1 s1 ->
-      exists i, exists s2, initial_state L2 s2 /\ fsim_match_states i s1 s2;
+      exists i, exists s2, initial_state L2 s2 /\ match_states i s1 s2;
     fsim_match_final_states:
       forall i s1 s2 r,
-      fsim_match_states i s1 s2 -> final_state L1 s1 r -> final_state L2 s2 r;
+      match_states i s1 s2 -> final_state L1 s1 r -> final_state L2 s2 r;
     fsim_simulation:
       forall s1 t s1', Step L1 s1 t s1' ->
-      forall i s2, fsim_match_states i s1 s2 ->
+      forall i s2, match_states i s1 s2 ->
       exists i', exists s2',
-         (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ fsim_order i' i))
-      /\ fsim_match_states i' s1' s2';
+         (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ order i' i))
+      /\ match_states i' s1' s2';
     fsim_public_preserved:
       forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id
   }.
 
-Implicit Arguments forward_simulation [].
+Arguments fsim_properties: clear implicits.
+
+Inductive forward_simulation (L1 L2: semantics) : Prop :=
+  Forward_simulation (index: Type)
+                     (order: index -> index -> Prop)
+                     (match_states: index -> state L1 -> state L2 -> Prop)
+                     (props: fsim_properties L1 L2 index order match_states).
+
+Arguments Forward_simulation {L1 L2 index} order match_states props.
 
 (** An alternate form of the simulation diagram *)
 
 Lemma fsim_simulation':
-  forall L1 L2 (S: forward_simulation L1 L2),
+  forall L1 L2 index order match_states, fsim_properties L1 L2 index order match_states ->
   forall i s1 t s1', Step L1 s1 t s1' ->
-  forall s2, S i s1 s2 ->
-  (exists i', exists s2', Plus L2 s2 t s2' /\ S i' s1' s2')
-  \/ (exists i', fsim_order S i' i /\ t = E0 /\ S i' s1' s2).
+  forall s2, match_states i s1 s2 ->
+  (exists i', exists s2', Plus L2 s2 t s2' /\ match_states i' s1' s2')
+  \/ (exists i', order i' i /\ t = E0 /\ match_states i' s1' s2).
 Proof.
   intros. exploit fsim_simulation; eauto.
   intros [i' [s2' [A B]]]. intuition.
   left; exists i'; exists s2'; auto.
-  inv H2.
+  inv H3.
   right; exists i'; auto.
   left; exists i'; exists s2'; split; auto. econstructor; eauto.
 Qed.
@@ -602,15 +608,15 @@ Hypothesis simulation:
 
 Lemma forward_simulation_star_wf: forward_simulation L1 L2.
 Proof.
-  apply Forward_simulation with
-    (fsim_order := order)
-    (fsim_match_states := fun idx s1 s2 => idx = s1 /\ match_states s1 s2);
-  auto.
-  intros. exploit match_initial_states; eauto. intros [s2 [A B]].
+  apply Forward_simulation with order (fun idx s1 s2 => idx = s1 /\ match_states s1 s2);
+  constructor.
+- auto.
+- intros. exploit match_initial_states; eauto. intros [s2 [A B]].
     exists s1; exists s2; auto.
-  intros. destruct H. eapply match_final_states; eauto.
-  intros. destruct H0. subst i. exploit simulation; eauto. intros [s2' [A B]].
-  exists s1'; exists s2'; intuition.
+- intros. destruct H. eapply match_final_states; eauto.
+- intros. destruct H0. subst i. exploit simulation; eauto. intros [s2' [A B]].
+  exists s1'; exists s2'; intuition auto.
+- auto.
 Qed.
 
 End SIMULATION_STAR_WF.
@@ -709,28 +715,26 @@ End FORWARD_SIMU_DIAGRAMS.
 
 Section SIMULATION_SEQUENCES.
 
-Variable L1: semantics.
-Variable L2: semantics.
-Variable S: forward_simulation L1 L2.
+Context L1 L2 index order match_states (S: fsim_properties L1 L2 index order match_states).
 
 Lemma simulation_star:
   forall s1 t s1', Star L1 s1 t s1' ->
-  forall i s2, S i s1 s2 ->
-  exists i', exists s2', Star L2 s2 t s2' /\ S i' s1' s2'.
+  forall i s2, match_states i s1 s2 ->
+  exists i', exists s2', Star L2 s2 t s2' /\ match_states i' s1' s2'.
 Proof.
   induction 1; intros.
   exists i; exists s2; split; auto. apply star_refl.
   exploit fsim_simulation; eauto. intros [i' [s2' [A B]]].
   exploit IHstar; eauto. intros [i'' [s2'' [C D]]].
   exists i''; exists s2''; split; auto. eapply star_trans; eauto.
-  intuition. apply plus_star; auto.
+  intuition auto. apply plus_star; auto.
 Qed.
 
 Lemma simulation_plus:
   forall s1 t s1', Plus L1 s1 t s1' ->
-  forall i s2, S i s1 s2 ->
-  (exists i', exists s2', Plus L2 s2 t s2' /\ S i' s1' s2')
-  \/ (exists i', clos_trans _ (fsim_order S) i' i /\ t = E0 /\ S i' s1' s2).
+  forall i s2, match_states i s1 s2 ->
+  (exists i', exists s2', Plus L2 s2 t s2' /\ match_states i' s1' s2')
+  \/ (exists i', clos_trans _ order i' i /\ t = E0 /\ match_states i' s1' s2).
 Proof.
   induction 1 using plus_ind2; intros.
 (* base case *)
@@ -744,34 +748,34 @@ Proof.
   left; exists i''; exists s2''; split; auto. eapply plus_star_trans; eauto.
   exploit IHplus; eauto. intros [[i'' [s2'' [P Q]]] | [i'' [P [Q R]]]].
   subst. simpl. left; exists i''; exists s2''; auto.
-  subst. simpl. right; exists i''; intuition.
+  subst. simpl. right; exists i''; intuition auto.
   eapply t_trans; eauto. eapply t_step; eauto.
 Qed.
 
 Lemma simulation_forever_silent:
   forall i s1 s2,
-  Forever_silent L1 s1 -> S i s1 s2 ->
+  Forever_silent L1 s1 -> match_states i s1 s2 ->
   Forever_silent L2 s2.
 Proof.
   assert (forall i s1 s2,
-          Forever_silent L1 s1 -> S i s1 s2 ->
-          forever_silent_N (step L2) (fsim_order S) (globalenv L2) i s2).
+          Forever_silent L1 s1 -> match_states i s1 s2 ->
+          forever_silent_N (step L2) order (globalenv L2) i s2).
     cofix COINDHYP; intros.
     inv H. destruct (fsim_simulation S _ _ _ H1 _ _ H0) as [i' [s2' [A B]]].
     destruct A as [C | [C D]].
     eapply forever_silent_N_plus; eauto.
     eapply forever_silent_N_star; eauto.
-  intros. eapply forever_silent_N_forever; eauto. apply fsim_order_wf.
+  intros. eapply forever_silent_N_forever; eauto. eapply fsim_order_wf; eauto.
 Qed.
 
 Lemma simulation_forever_reactive:
   forall i s1 s2 T,
-  Forever_reactive L1 s1 T -> S i s1 s2 ->
+  Forever_reactive L1 s1 T -> match_states i s1 s2 ->
   Forever_reactive L2 s2 T.
 Proof.
   cofix COINDHYP; intros.
   inv H.
-  destruct (simulation_star H1 i _ H0) as [i' [st2' [A B]]].
+  edestruct simulation_star as [i' [st2' [A B]]]; eauto.
   econstructor; eauto.
 Qed.
 
@@ -779,56 +783,48 @@ End SIMULATION_SEQUENCES.
 
 (** ** Composing two forward simulations *)
 
-Section COMPOSE_SIMULATIONS.
-
-Variable L1: semantics.
-Variable L2: semantics.
-Variable L3: semantics.
-Variable S12: forward_simulation L1 L2.
-Variable S23: forward_simulation L2 L3.
-
-Let ff_index : Type := (fsim_index S23 * fsim_index S12)%type.
-
-Let ff_order : ff_index -> ff_index -> Prop :=
-  lex_ord (clos_trans _ (fsim_order S23)) (fsim_order S12).
-
-Let ff_match_states (i: ff_index) (s1: state L1) (s3: state L3) : Prop :=
-  exists s2, S12 (snd i) s1 s2 /\ S23 (fst i) s2 s3.
-
-Lemma compose_forward_simulation: forward_simulation L1 L3.
-Proof.
-  apply Forward_simulation with (fsim_order := ff_order) (fsim_match_states := ff_match_states).
-(* well founded *)
-  unfold ff_order. apply wf_lex_ord. apply wf_clos_trans. apply fsim_order_wf. apply fsim_order_wf.
-(* initial states *)
-  intros. exploit (fsim_match_initial_states S12); eauto. intros [i [s2 [A B]]].
-  exploit (fsim_match_initial_states S23); eauto. intros [i' [s3 [C D]]].
+Lemma compose_forward_simulations:
+  forall L1 L2 L3, forward_simulation L1 L2 -> forward_simulation L2 L3 -> forward_simulation L1 L3.
+Proof.
+  intros L1 L2 L3 S12 S23. 
+  destruct S12 as [index order match_states props].
+  destruct S23 as [index' order' match_states' props'].
+
+  set (ff_index := (index' * index)%type).
+  set (ff_order := lex_ord (clos_trans _ order') order).
+  set (ff_match_states := fun (i: ff_index) (s1: state L1) (s3: state L3) =>
+                             exists s2, match_states (snd i) s1 s2 /\ match_states' (fst i) s2 s3).
+  apply Forward_simulation with ff_order ff_match_states; constructor.
+- (* well founded *)
+  unfold ff_order. apply wf_lex_ord. apply wf_clos_trans.
+  eapply fsim_order_wf; eauto. eapply fsim_order_wf; eauto.
+- (* initial states *)
+  intros. exploit (fsim_match_initial_states props); eauto. intros [i [s2 [A B]]].
+  exploit (fsim_match_initial_states props'); eauto. intros [i' [s3 [C D]]].
   exists (i', i); exists s3; split; auto. exists s2; auto.
-(* final states *)
+- (* final states *)
   intros. destruct H as [s3 [A B]].
-  eapply (fsim_match_final_states S23); eauto.
-  eapply (fsim_match_final_states S12); eauto.
-(* simulation *)
+  eapply (fsim_match_final_states props'); eauto.
+  eapply (fsim_match_final_states props); eauto.
+- (* simulation *)
   intros. destruct H0 as [s3 [A B]]. destruct i as [i2 i1]; simpl in *.
-  exploit (fsim_simulation' S12); eauto. intros [[i1' [s3' [C D]]] | [i1' [C [D E]]]].
-  (* L2 makes one or several steps. *)
+  exploit (fsim_simulation' props); eauto. intros [[i1' [s3' [C D]]] | [i1' [C [D E]]]].
++ (* L2 makes one or several steps. *)
   exploit simulation_plus; eauto. intros [[i2' [s2' [P Q]]] | [i2' [P [Q R]]]].
-  (* L3 makes one or several steps *)
+* (* L3 makes one or several steps *)
   exists (i2', i1'); exists s2'; split. auto. exists s3'; auto.
-  (* L3 makes no step *)
+* (* L3 makes no step *)
   exists (i2', i1'); exists s2; split.
   right; split. subst t; apply star_refl. red. left. auto.
   exists s3'; auto.
-  (* L2 makes no step *)
++ (* L2 makes no step *)
   exists (i2, i1'); exists s2; split.
   right; split. subst t; apply star_refl. red. right. auto.
   exists s3; auto.
-(* symbols *)
-  intros. transitivity (Senv.public_symbol (symbolenv L2) id); apply fsim_public_preserved; auto.
+- (* symbols *)
+  intros. transitivity (Senv.public_symbol (symbolenv L2) id); eapply fsim_public_preserved; eauto.
 Qed.
 
-End COMPOSE_SIMULATIONS.
-
 (** * Receptiveness and determinacy *)
 
 Definition single_events (L: semantics) : Prop :=
@@ -916,49 +912,57 @@ Qed.
 
 (** The general form of a backward simulation. *)
 
-Record backward_simulation (L1 L2: semantics) : Type :=
-  Backward_simulation {
-    bsim_index: Type;
-    bsim_order: bsim_index -> bsim_index -> Prop;
-    bsim_order_wf: well_founded bsim_order;
-    bsim_match_states :> bsim_index -> state L1 -> state L2 -> Prop;
+Record bsim_properties (L1 L2: semantics) (index: Type)
+                       (order: index -> index -> Prop)
+                       (match_states: index -> state L1 -> state L2 -> Prop) : Prop := {
+    bsim_order_wf: well_founded order;
     bsim_initial_states_exist:
       forall s1, initial_state L1 s1 -> exists s2, initial_state L2 s2;
     bsim_match_initial_states:
       forall s1 s2, initial_state L1 s1 -> initial_state L2 s2 ->
-      exists i, exists s1', initial_state L1 s1' /\ bsim_match_states i s1' s2;
+      exists i, exists s1', initial_state L1 s1' /\ match_states i s1' s2;
     bsim_match_final_states:
       forall i s1 s2 r,
-      bsim_match_states i s1 s2 -> safe L1 s1 -> final_state L2 s2 r ->
+      match_states i s1 s2 -> safe L1 s1 -> final_state L2 s2 r ->
       exists s1', Star L1 s1 E0 s1' /\ final_state L1 s1' r;
     bsim_progress:
       forall i s1 s2,
-      bsim_match_states i s1 s2 -> safe L1 s1 ->
+      match_states i s1 s2 -> safe L1 s1 ->
       (exists r, final_state L2 s2 r) \/
       (exists t, exists s2', Step L2 s2 t s2');
     bsim_simulation:
       forall s2 t s2', Step L2 s2 t s2' ->
-      forall i s1, bsim_match_states i s1 s2 -> safe L1 s1 ->
+      forall i s1, match_states i s1 s2 -> safe L1 s1 ->
       exists i', exists s1',
-         (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order i' i))
-      /\ bsim_match_states i' s1' s2';
+         (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ order i' i))
+      /\ match_states i' s1' s2';
     bsim_public_preserved:
       forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id
   }.
 
+Arguments bsim_properties: clear implicits.
+
+Inductive backward_simulation (L1 L2: semantics) : Prop :=
+  Backward_simulation (index: Type)
+                      (order: index -> index -> Prop)
+                      (match_states: index -> state L1 -> state L2 -> Prop)
+                      (props: bsim_properties L1 L2 index order match_states).
+
+Arguments Backward_simulation {L1 L2 index} order match_states props.
+
 (** An alternate form of the simulation diagram *)
 
 Lemma bsim_simulation':
-  forall L1 L2 (S: backward_simulation L1 L2),
+  forall L1 L2 index order match_states, bsim_properties L1 L2 index order match_states ->
   forall i s2 t s2', Step L2 s2 t s2' ->
-  forall s1, S i s1 s2 -> safe L1 s1 ->
-  (exists i', exists s1', Plus L1 s1 t s1' /\ S i' s1' s2')
-  \/ (exists i', bsim_order S i' i /\ t = E0 /\ S i' s1 s2').
+  forall s1, match_states i s1 s2 -> safe L1 s1 ->
+  (exists i', exists s1', Plus L1 s1 t s1' /\ match_states i' s1' s2')
+  \/ (exists i', order i' i /\ t = E0 /\ match_states i' s1 s2').
 Proof.
   intros. exploit bsim_simulation; eauto.
   intros [i' [s1' [A B]]]. intuition.
   left; exists i'; exists s1'; auto.
-  inv H3.
+  inv H4.
   right; exists i'; auto.
   left; exists i'; exists s1'; split; auto. econstructor; eauto.
 Qed.
@@ -1004,13 +1008,13 @@ Hypothesis simulation:
 Lemma backward_simulation_plus: backward_simulation L1 L2.
 Proof.
   apply Backward_simulation with
-    (bsim_order := fun (x y: unit) => False)
-    (bsim_match_states := fun (i: unit) s1 s2 => match_states s1 s2);
-  auto.
-  red; intros; constructor; intros. contradiction.
-  intros. exists tt; eauto.
-  intros. exists s1; split. apply star_refl. eauto.
-  intros. exploit simulation; eauto. intros [s1' [A B]].
+    (fun (x y: unit) => False)
+    (fun (i: unit) s1 s2 => match_states s1 s2);
+  constructor; auto.
+- red; intros; constructor; intros. contradiction.
+- intros. exists tt; eauto.
+- intros. exists s1; split. apply star_refl. eauto.
+- intros. exploit simulation; eauto. intros [s1' [A B]].
   exists tt; exists s1'; auto.
 Qed.
 
@@ -1022,19 +1026,17 @@ End BACKWARD_SIMU_DIAGRAMS.
 
 Section BACKWARD_SIMULATION_SEQUENCES.
 
-Variable L1: semantics.
-Variable L2: semantics.
-Variable S: backward_simulation L1 L2.
+Context L1 L2 index order match_states (S: bsim_properties L1 L2 index order match_states).
 
 Lemma bsim_E0_star:
   forall s2 s2', Star L2 s2 E0 s2' ->
-  forall i s1, S i s1 s2 -> safe L1 s1 ->
-  exists i', exists s1', Star L1 s1 E0 s1' /\ S i' s1' s2'.
+  forall i s1, match_states i s1 s2 -> safe L1 s1 ->
+  exists i', exists s1', Star L1 s1 E0 s1' /\ match_states i' s1' s2'.
 Proof.
   intros s20 s20' STAR0. pattern s20, s20'. eapply star_E0_ind; eauto.
-(* base case *)
+- (* base case *)
   intros. exists i; exists s1; split; auto. apply star_refl.
-(* inductive case *)
+- (* inductive case *)
   intros. exploit bsim_simulation; eauto. intros [i' [s1' [A B]]].
   assert (Star L1 s0 E0 s1'). intuition. apply plus_star; auto.
   exploit H0. eauto. eapply star_safe; eauto. intros [i'' [s1'' [C D]]].
@@ -1043,7 +1045,7 @@ Qed.
 
 Lemma bsim_safe:
   forall i s1 s2,
-  S i s1 s2 -> safe L1 s1 -> safe L2 s2.
+  match_states i s1 s2 -> safe L1 s1 -> safe L2 s2.
 Proof.
   intros; red; intros.
   exploit bsim_E0_star; eauto. intros [i' [s1' [A B]]].
@@ -1052,22 +1054,22 @@ Qed.
 
 Lemma bsim_E0_plus:
   forall s2 t s2', Plus L2 s2 t s2' -> t = E0 ->
-  forall i s1, S i s1 s2 -> safe L1 s1 ->
-     (exists i', exists s1', Plus L1 s1 E0 s1' /\ S i' s1' s2')
-  \/ (exists i', clos_trans _ (bsim_order S) i' i /\ S i' s1 s2').
+  forall i s1, match_states i s1 s2 -> safe L1 s1 ->
+     (exists i', exists s1', Plus L1 s1 E0 s1' /\ match_states i' s1' s2')
+  \/ (exists i', clos_trans _ order i' i /\ match_states i' s1 s2').
 Proof.
   induction 1 using plus_ind2; intros; subst t.
-(* base case *)
+- (* base case *)
   exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]].
-  left; exists i'; exists s1'; auto.
-  right; exists i'; intuition.
-(* inductive case *)
++ left; exists i'; exists s1'; auto.
++ right; exists i'; intuition.
+- (* inductive case *)
   exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst.
   exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]].
-  exploit bsim_E0_star. apply plus_star; eauto. eauto. eapply star_safe; eauto. apply plus_star; auto.
++ exploit bsim_E0_star. apply plus_star; eauto. eauto. eapply star_safe; eauto. apply plus_star; auto.
   intros [i'' [s1'' [P Q]]].
   left; exists i''; exists s1''; intuition. eapply plus_star_trans; eauto.
-  exploit IHplus; eauto. intros [P | [i'' [P Q]]].
++ exploit IHplus; eauto. intros [P | [i'' [P Q]]].
   left; auto.
   right; exists i''; intuition. eapply t_trans; eauto. apply t_step; auto.
 Qed.
@@ -1098,21 +1100,20 @@ Variable L1: semantics.
 Variable L2: semantics.
 Variable L3: semantics.
 Hypothesis L3_single_events: single_events L3.
-Variable S12: backward_simulation L1 L2.
-Variable S23: backward_simulation L2 L3.
+Context index order match_states (S12: bsim_properties L1 L2 index order match_states).
+Context index' order' match_states' (S23: bsim_properties L2 L3 index' order' match_states').
 
-Let bb_index : Type := (bsim_index S12 * bsim_index S23)%type.
+Let bb_index : Type := (index * index')%type.
 
-Let bb_order : bb_index -> bb_index -> Prop :=
-  lex_ord (clos_trans _ (bsim_order S12)) (bsim_order S23).
+Definition bb_order : bb_index -> bb_index -> Prop := lex_ord (clos_trans _ order) order'.
 
 Inductive bb_match_states: bb_index -> state L1 -> state L3 -> Prop :=
   | bb_match_later: forall i1 i2 s1 s3 s2x s2y,
-      S12 i1 s1 s2x -> Star L2 s2x E0 s2y -> S23 i2 s2y s3 ->
+      match_states i1 s1 s2x -> Star L2 s2x E0 s2y -> match_states' i2 s2y s3 ->
       bb_match_states (i1, i2) s1 s3.
 
 Lemma bb_match_at: forall i1 i2 s1 s3 s2,
-  S12 i1 s1 s2 -> S23 i2 s2 s3 ->
+  match_states i1 s1 s2 -> match_states' i2 s2 s3 ->
   bb_match_states (i1, i2) s1 s3.
 Proof.
   intros. econstructor; eauto. apply star_refl.
@@ -1120,7 +1121,7 @@ Qed.
 
 Lemma bb_simulation_base:
   forall s3 t s3', Step L3 s3 t s3' ->
-  forall i1 s1 i2 s2, S12 i1 s1 s2 -> S23 i2 s2 s3 -> safe L1 s1 ->
+  forall i1 s1 i2 s2, match_states i1 s1 s2 -> match_states' i2 s2 s3 -> safe L1 s1 ->
   exists i', exists s1',
     (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bb_order i' (i1, i2)))
     /\ bb_match_states i' s1' s3'.
@@ -1128,29 +1129,29 @@ Proof.
   intros.
   exploit (bsim_simulation' S23); eauto. eapply bsim_safe; eauto.
   intros [ [i2' [s2' [PLUS2 MATCH2]]] | [i2' [ORD2 [EQ MATCH2]]]].
-  (* 1 L2 makes one or several transitions *)
+- (* 1 L2 makes one or several transitions *)
   assert (EITHER: t = E0 \/ (length t = 1)%nat).
-    exploit L3_single_events; eauto.
-    destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction.
+  { exploit L3_single_events; eauto.
+    destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction. }
   destruct EITHER.
-  (* 1.1 these are silent transitions *)
-  subst t. exploit bsim_E0_plus; eauto.
++ (* 1.1 these are silent transitions *)
+  subst t. exploit (bsim_E0_plus S12); eauto.
   intros [ [i1' [s1' [PLUS1 MATCH1]]] | [i1' [ORD1 MATCH1]]].
-  (* 1.1.1 L1 makes one or several transitions *)
+* (* 1.1.1 L1 makes one or several transitions *)
   exists (i1', i2'); exists s1'; split. auto. eapply bb_match_at; eauto.
-  (* 1.1.2 L1 makes no transitions *)
+* (* 1.1.2 L1 makes no transitions *)
   exists (i1', i2'); exists s1; split.
   right; split. apply star_refl. left; auto.
   eapply bb_match_at; eauto.
-  (* 1.2 non-silent transitions *)
++ (* 1.2 non-silent transitions *)
   exploit star_non_E0_split. apply plus_star; eauto. auto.
   intros [s2x [s2y [P [Q R]]]].
-  exploit bsim_E0_star. eexact P. eauto. auto. intros [i1' [s1x [X Y]]].
-  exploit bsim_simulation'. eexact Q. eauto. eapply star_safe; eauto.
+  exploit (bsim_E0_star S12). eexact P. eauto. auto. intros [i1' [s1x [X Y]]].
+  exploit (bsim_simulation' S12). eexact Q. eauto. eapply star_safe; eauto.
   intros [[i1'' [s1y [U V]]] | [i1'' [U [V W]]]]; try (subst t; discriminate).
   exists (i1'', i2'); exists s1y; split.
   left. eapply star_plus_trans; eauto. eapply bb_match_later; eauto.
-  (* 2. L2 makes no transitions *)
+- (* 2. L2 makes no transitions *)
   subst. exists (i1, i2'); exists s1; split.
   right; split. apply star_refl. right; auto.
   eapply bb_match_at; eauto.
@@ -1165,12 +1166,12 @@ Lemma bb_simulation:
 Proof.
   intros. inv H0.
   exploit star_inv; eauto. intros [[EQ1 EQ2] | PLUS].
-  (* 1. match at *)
+- (* 1. match at *)
   subst. eapply bb_simulation_base; eauto.
-  (* 2. match later *)
-  exploit bsim_E0_plus; eauto.
+- (* 2. match later *)
+  exploit (bsim_E0_plus S12); eauto.
   intros [[i1' [s1' [A B]]] | [i1' [A B]]].
-  (* 2.1 one or several silent transitions *)
++ (* 2.1 one or several silent transitions *)
   exploit bb_simulation_base. eauto. auto. eexact B. eauto.
     eapply star_safe; eauto. eapply plus_star; eauto.
   intros [i'' [s1'' [C D]]].
@@ -1178,7 +1179,7 @@ Proof.
   left. eapply plus_star_trans; eauto.
   destruct C as [P | [P Q]]. apply plus_star; eauto. eauto.
   traceEq.
-  (* 2.2 no silent transition *)
++ (* 2.2 no silent transition *)
   exploit bb_simulation_base. eauto. auto. eexact B. eauto. auto.
   intros [i'' [s1'' [C D]]].
   exists i''; exists s1''; split; auto.
@@ -1186,48 +1187,53 @@ Proof.
   inv H6. left. eapply t_trans; eauto. left; auto.
 Qed.
 
-Lemma compose_backward_simulation: backward_simulation L1 L3.
-Proof.
-  apply Backward_simulation with (bsim_order := bb_order) (bsim_match_states := bb_match_states).
-(* well founded *)
-  unfold bb_order. apply wf_lex_ord. apply wf_clos_trans. apply bsim_order_wf. apply bsim_order_wf.
-(* initial states exist *)
-  intros. exploit (bsim_initial_states_exist S12); eauto. intros [s2 A].
-  eapply (bsim_initial_states_exist S23); eauto.
-(* match initial states *)
+End COMPOSE_BACKWARD_SIMULATIONS.
+
+Lemma compose_backward_simulation:
+  forall L1 L2 L3,
+  single_events L3 -> backward_simulation L1 L2 -> backward_simulation L2 L3 ->
+  backward_simulation L1 L3.
+Proof.
+  intros L1 L2 L3 L3single S12 S23.
+  destruct S12 as [index order match_states props].
+  destruct S23 as [index' order' match_states' props'].
+  apply Backward_simulation with (bb_order order order') (bb_match_states L1 L2 L3 match_states match_states');
+  constructor.
+- (* well founded *)
+  unfold bb_order. apply wf_lex_ord. apply wf_clos_trans. eapply bsim_order_wf; eauto. eapply bsim_order_wf; eauto.
+- (* initial states exist *)
+  intros. exploit (bsim_initial_states_exist props); eauto. intros [s2 A].
+  eapply (bsim_initial_states_exist props'); eauto.
+- (* match initial states *)
   intros s1 s3 INIT1 INIT3.
-  exploit (bsim_initial_states_exist S12); eauto. intros [s2 INIT2].
-  exploit (bsim_match_initial_states S23); eauto. intros [i2 [s2' [INIT2' M2]]].
-  exploit (bsim_match_initial_states S12); eauto. intros [i1 [s1' [INIT1' M1]]].
-  exists (i1, i2); exists s1'; intuition. eapply bb_match_at; eauto.
-(* match final states *)
+  exploit (bsim_initial_states_exist props); eauto. intros [s2 INIT2].
+  exploit (bsim_match_initial_states props'); eauto. intros [i2 [s2' [INIT2' M2]]].
+  exploit (bsim_match_initial_states props); eauto. intros [i1 [s1' [INIT1' M1]]].
+  exists (i1, i2); exists s1'; intuition auto. eapply bb_match_at; eauto.
+- (* match final states *)
   intros i s1 s3 r MS SAFE FIN. inv MS.
-  exploit (bsim_match_final_states S23); eauto.
+  exploit (bsim_match_final_states props'); eauto.
     eapply star_safe; eauto. eapply bsim_safe; eauto.
   intros [s2' [A B]].
-  exploit bsim_E0_star. eapply star_trans. eexact H0. eexact A. auto. eauto. auto.
+  exploit (bsim_E0_star props). eapply star_trans. eexact H0. eexact A. auto. eauto. auto.
   intros [i1' [s1' [C D]]].
-  exploit (bsim_match_final_states S12); eauto. eapply star_safe; eauto.
+  exploit (bsim_match_final_states props); eauto. eapply star_safe; eauto.
   intros [s1'' [P Q]].
   exists s1''; split; auto. eapply star_trans; eauto.
-(* progress *)
+- (* progress *)
   intros i s1 s3 MS SAFE. inv MS.
-  eapply (bsim_progress S23). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto.
-(* simulation *)
-  exact bb_simulation.
-(* symbols *)
-  intros. transitivity (Senv.public_symbol (symbolenv L2) id); apply bsim_public_preserved; auto.
+  eapply (bsim_progress props'). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto.
+- (* simulation *)
+  apply bb_simulation; auto.
+- (* symbols *)
+  intros. transitivity (Senv.public_symbol (symbolenv L2) id); eapply bsim_public_preserved; eauto.
 Qed.
 
-End COMPOSE_BACKWARD_SIMULATIONS.
-
 (** ** Converting a forward simulation to a backward simulation *)
 
 Section FORWARD_TO_BACKWARD.
 
-Variable L1: semantics.
-Variable L2: semantics.
-Variable FS: forward_simulation L1 L2.
+Context L1 L2 index order match_states (FS: fsim_properties L1 L2 index order match_states).
 Hypothesis L1_receptive: receptive L1.
 Hypothesis L2_determinate: determinate L2.
 
@@ -1243,38 +1249,38 @@ Inductive f2b_transitions: state L1 -> state L2 -> Prop :=
       Star L1 s1 E0 s1' ->
       Step L1 s1' t s1'' ->
       Plus L2 s2 t s2' ->
-      FS i' s1' s2 ->
-      FS i'' s1'' s2' ->
+      match_states i' s1' s2 ->
+      match_states i'' s1'' s2' ->
       f2b_transitions s1 s2.
 
 Lemma f2b_progress:
-  forall i s1 s2, FS i s1 s2 -> safe L1 s1 -> f2b_transitions s1 s2.
+  forall i s1 s2, match_states i s1 s2 -> safe L1 s1 -> f2b_transitions s1 s2.
 Proof.
-  intros i0; pattern i0. apply well_founded_ind with (R := fsim_order FS).
-  apply fsim_order_wf.
+  intros i0; pattern i0. apply well_founded_ind with (R := order).
+  eapply fsim_order_wf; eauto.
   intros i REC s1 s2 MATCH SAFE.
   destruct (SAFE s1) as [[r FINAL] | [t [s1' STEP1]]]. apply star_refl.
-  (* final state reached *)
+- (* final state reached *)
   eapply f2b_trans_final; eauto.
   apply star_refl.
   eapply fsim_match_final_states; eauto.
-  (* L1 can make one step *)
+- (* L1 can make one step *)
   exploit (fsim_simulation FS); eauto. intros [i' [s2' [A MATCH']]].
-  assert (B: Plus L2 s2 t s2' \/ (s2' = s2 /\ t = E0 /\ fsim_order FS i' i)).
-    intuition.
-    destruct (star_inv H0); intuition.
+  assert (B: Plus L2 s2 t s2' \/ (s2' = s2 /\ t = E0 /\ order i' i)).
+    intuition auto.
+    destruct (star_inv H0); intuition auto.
   clear A. destruct B as [PLUS2 | [EQ1 [EQ2 ORDER]]].
-  eapply f2b_trans_step; eauto. apply star_refl.
-  subst. exploit REC; eauto. eapply star_safe; eauto. apply star_one; auto.
++ eapply f2b_trans_step; eauto. apply star_refl.
++ subst. exploit REC; eauto. eapply star_safe; eauto. apply star_one; auto.
   intros TRANS; inv TRANS.
-  eapply f2b_trans_final; eauto. eapply star_left; eauto.
-  eapply f2b_trans_step; eauto. eapply star_left; eauto.
+* eapply f2b_trans_final; eauto. eapply star_left; eauto.
+* eapply f2b_trans_step; eauto. eapply star_left; eauto.
 Qed.
 
 Lemma fsim_simulation_not_E0:
   forall s1 t s1', Step L1 s1 t s1' -> t <> E0 ->
-  forall i s2, FS i s1 s2 ->
-  exists i', exists s2', Plus L2 s2 t s2' /\ FS i' s1' s2'.
+  forall i s2, match_states i s1 s2 ->
+  exists i', exists s2', Plus L2 s2 t s2' /\ match_states i' s1' s2'.
 Proof.
   intros. exploit (fsim_simulation FS); eauto. intros [i' [s2' [A B]]].
   exists i'; exists s2'; split; auto.
@@ -1363,23 +1369,23 @@ Qed.
 
 Inductive f2b_match_states: f2b_index -> state L1 -> state L2 -> Prop :=
   | f2b_match_at: forall i s1 s2,
-      FS i s1 s2 ->
+      match_states i s1 s2 ->
       f2b_match_states (F2BI_after O) s1 s2
   | f2b_match_before: forall s1 t s1' s2b s2 n s2a i,
       Step L1 s1 t s1' ->  t <> E0 ->
       Star L2 s2b E0 s2 ->
       starN (step L2) (globalenv L2) n s2 t s2a ->
-      FS i s1 s2b ->
+      match_states i s1 s2b ->
       f2b_match_states (F2BI_before n) s1 s2
   | f2b_match_after: forall n s2 s2a s1 i,
       starN (step L2) (globalenv L2) (S n) s2 E0 s2a ->
-      FS i s1 s2a ->
+      match_states i s1 s2a ->
       f2b_match_states (F2BI_after (S n)) s1 s2.
 
 Remark f2b_match_after':
   forall n s2 s2a s1 i,
   starN (step L2) (globalenv L2) n s2 E0 s2a ->
-  FS i s1 s2a ->
+  match_states i s1 s2a ->
   f2b_match_states (F2BI_after n) s1 s2.
 Proof.
   intros. inv H.
@@ -1398,15 +1404,15 @@ Lemma f2b_simulation_step:
 Proof.
   intros s2 t s2' STEP2 i s1 MATCH SAFE.
   inv MATCH.
-(* 1. At matching states *)
+- (* 1. At matching states *)
   exploit f2b_progress; eauto. intros TRANS; inv TRANS.
-  (* 1.1  L1 can reach final state and L2 is at final state: impossible! *)
++ (* 1.1  L1 can reach final state and L2 is at final state: impossible! *)
   exploit (sd_final_nostep L2_determinate); eauto. contradiction.
-  (* 1.2  L1 can make 0 or several steps; L2 can make 1 or several matching steps. *)
++ (* 1.2  L1 can make 0 or several steps; L2 can make 1 or several matching steps. *)
   inv H2.
   exploit f2b_determinacy_inv. eexact H5. eexact STEP2.
   intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
-  (* 1.2.1  L2 makes a silent transition *)
+* (* 1.2.1  L2 makes a silent transition *)
   destruct (silent_or_not_silent t2).
   (* 1.2.1.1  L1 makes a silent transition too: perform transition now and go to "after" state *)
   subst. simpl in *. destruct (star_starN H6) as [n STEPS2].
@@ -1418,7 +1424,7 @@ Proof.
   exists (F2BI_before n); exists s1'; split.
   right; split. auto. constructor.
   econstructor. eauto. auto. apply star_one; eauto. eauto. eauto.
-  (* 1.2.2 L2 makes a non-silent transition, and so does L1 *)
+* (* 1.2.2 L2 makes a non-silent transition, and so does L1 *)
   exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ].
   congruence.
   subst t2. rewrite E0_right in H1.
@@ -1437,15 +1443,15 @@ Proof.
   left. eapply plus_right; eauto.
   eapply f2b_match_after'; eauto.
 
-(* 2. Before *)
+- (* 2. Before *)
   inv H2. congruence.
   exploit f2b_determinacy_inv. eexact H4. eexact STEP2.
   intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
-  (* 2.1 L2 makes a silent transition: remain in "before" state *)
++ (* 2.1 L2 makes a silent transition: remain in "before" state *)
   subst. simpl in *. exists (F2BI_before n0); exists s1; split.
   right; split. apply star_refl. constructor. omega.
   econstructor; eauto. eapply star_right; eauto.
-  (* 2.2 L2 make a non-silent transition *)
++ (* 2.2 L2 make a non-silent transition *)
   exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ].
   congruence.
   subst. rewrite E0_right in *.
@@ -1466,7 +1472,7 @@ Proof.
   left. apply plus_one; auto.
   eapply f2b_match_after'; eauto.
 
-(* 3. After *)
+- (* 3. After *)
   inv H. exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst.
   exploit f2b_determinacy_inv. eexact H2. eexact STEP2.
   intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
@@ -1476,20 +1482,28 @@ Proof.
   congruence.
 Qed.
 
+End FORWARD_TO_BACKWARD.
+
 (** The backward simulation *)
 
-Lemma forward_to_backward_simulation: backward_simulation L1 L2.
+Lemma forward_to_backward_simulation:
+  forall L1 L2,
+  forward_simulation L1 L2 -> receptive L1 -> determinate L2 ->
+  backward_simulation L1 L2.
 Proof.
-  apply Backward_simulation with (bsim_order := f2b_order) (bsim_match_states := f2b_match_states).
+  intros L1 L2 FS L1_receptive L2_determinate.
+  destruct FS as [index order match_states FS].
+  apply Backward_simulation with f2b_order (f2b_match_states L1 L2 match_states); constructor.
+- (* well founded *)
   apply wf_f2b_order.
-(* initial states exist *)
+- (* initial states exist *)
   intros. exploit (fsim_match_initial_states FS); eauto. intros [i [s2 [A B]]].
   exists s2; auto.
-(* initial states *)
+- (* initial states *)
   intros. exploit (fsim_match_initial_states FS); eauto. intros [i [s2' [A B]]].
   assert (s2 = s2') by (eapply sd_initial_determ; eauto). subst s2'.
   exists (F2BI_after O); exists s1; split; auto. econstructor; eauto.
-(* final states *)
+- (* final states *)
   intros. inv H.
   exploit f2b_progress; eauto. intros TRANS; inv TRANS.
   assert (r0 = r) by (eapply (sd_final_determ L2_determinate); eauto). subst r0.
@@ -1497,21 +1511,19 @@ Proof.
   inv H4. exploit (sd_final_nostep L2_determinate); eauto. contradiction.
   inv H5. congruence. exploit (sd_final_nostep L2_determinate); eauto. contradiction.
   inv H2. exploit (sd_final_nostep L2_determinate); eauto. contradiction.
-(* progress *)
+- (* progress *)
   intros. inv H.
   exploit f2b_progress; eauto. intros TRANS; inv TRANS.
   left; exists r; auto.
   inv H3. right; econstructor; econstructor; eauto.
   inv H4. congruence. right; econstructor; econstructor; eauto.
   inv H1. right; econstructor; econstructor; eauto.
-(* simulation *)
-  exact f2b_simulation_step.
-(* symbols preserved *)
+- (* simulation *)
+  eapply f2b_simulation_step; eauto.
+- (* symbols preserved *)
   exact (fsim_public_preserved FS).
 Qed.
 
-End FORWARD_TO_BACKWARD.
-
 (** * Transforming a semantics into a single-event, equivalent semantics *)
 
 Definition well_behaved_traces (L: semantics) : Prop :=
@@ -1554,15 +1566,15 @@ Section FACTOR_FORWARD_SIMULATION.
 
 Variable L1: semantics.
 Variable L2: semantics.
-Variable sim: forward_simulation L1 L2.
+Context index order match_states (sim: fsim_properties L1 L2 index order match_states).
 Hypothesis L2single: single_events L2.
 
-Inductive ffs_match: fsim_index sim -> (trace * state L1) -> state L2 -> Prop :=
+Inductive ffs_match: index -> (trace * state L1) -> state L2 -> Prop :=
   | ffs_match_at: forall i s1 s2,
-      sim i s1 s2 ->
+      match_states i s1 s2 ->
       ffs_match i (E0, s1) s2
   | ffs_match_buffer: forall i ev t s1 s2 s2',
-      Star L2 s2 (ev :: t) s2' -> sim i s1 s2' ->
+      Star L2 s2 (ev :: t) s2' -> match_states i s1 s2' ->
       ffs_match i (ev :: t, s1) s2.
 
 Lemma star_non_E0_split':
@@ -1585,27 +1597,27 @@ Lemma ffs_simulation:
   forall s1 t s1', Step (atomic L1) s1 t s1' ->
   forall i s2, ffs_match i s1 s2 ->
   exists i', exists s2',
-     (Plus L2 s2 t s2' \/ (Star L2 s2 t s2') /\ fsim_order sim i' i)
+     (Plus L2 s2 t s2' \/ (Star L2 s2 t s2') /\ order i' i)
   /\ ffs_match i' s1' s2'.
 Proof.
   induction 1; intros.
-(* silent step *)
+- (* silent step *)
   inv H0.
   exploit (fsim_simulation sim); eauto.
   intros [i' [s2' [A B]]].
   exists i'; exists s2'; split. auto. constructor; auto.
-(* start step *)
+- (* start step *)
   inv H0.
   exploit (fsim_simulation sim); eauto.
   intros [i' [s2' [A B]]].
   destruct t as [ | ev' t].
-  (* single event *)
++ (* single event *)
   exists i'; exists s2'; split. auto. constructor; auto.
-  (* multiple events *)
++ (* multiple events *)
   assert (C: Star L2 s2 (ev :: ev' :: t) s2'). intuition. apply plus_star; auto.
   exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]].
   exists i'; exists s2x; split. auto. econstructor; eauto.
-(* continue step *)
+- (* continue step *)
   inv H0.
   exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]].
   destruct t.
@@ -1613,27 +1625,31 @@ Proof.
   exists i; exists s2x; split. auto. econstructor; eauto.
 Qed.
 
+End FACTOR_FORWARD_SIMULATION.
+
 Theorem factor_forward_simulation:
+  forall L1 L2,
+  forward_simulation L1 L2 -> single_events L2 ->
   forward_simulation (atomic L1) L2.
 Proof.
-  apply Forward_simulation with (fsim_match_states := ffs_match) (fsim_order := fsim_order sim).
-(* wf *)
-  apply fsim_order_wf.
-(* initial states *)
+  intros L1 L2 FS L2single. 
+  destruct FS as [index order match_states sim].
+  apply Forward_simulation with order (ffs_match L1 L2 match_states); constructor.
+- (* wf *)
+  eapply fsim_order_wf; eauto.
+- (* initial states *)
   intros. destruct s1 as [t1 s1]. simpl in H. destruct H. subst.
   exploit (fsim_match_initial_states sim); eauto. intros [i [s2 [A B]]].
   exists i; exists s2; split; auto. constructor; auto.
-(* final states *)
+- (* final states *)
   intros. destruct s1 as [t1 s1]. simpl in H0; destruct H0; subst. inv H.
   eapply (fsim_match_final_states sim); eauto.
-(* simulation *)
-  exact ffs_simulation.
-(* symbols preserved *)
+- (* simulation *)
+  eapply ffs_simulation; eauto.
+- (* symbols preserved *)
   simpl. exact (fsim_public_preserved sim).
 Qed.
 
-End FACTOR_FORWARD_SIMULATION.
-
 (** Likewise, a backward simulation from a single-event semantics [L1] to a semantics [L2]
   can be "factored" as a backward simulation from [L1] to [atomic L2]. *)
 
@@ -1641,13 +1657,13 @@ Section FACTOR_BACKWARD_SIMULATION.
 
 Variable L1: semantics.
 Variable L2: semantics.
-Variable sim: backward_simulation L1 L2.
+Context index order match_states (sim: bsim_properties L1 L2 index order match_states).
 Hypothesis L1single: single_events L1.
 Hypothesis L2wb: well_behaved_traces L2.
 
-Inductive fbs_match: bsim_index sim -> state L1 -> (trace * state L2) -> Prop :=
+Inductive fbs_match: index -> state L1 -> (trace * state L2) -> Prop :=
   | fbs_match_intro: forall i s1 t s2 s1',
-      Star L1 s1 t s1' -> sim i s1' s2 ->
+      Star L1 s1 t s1' -> match_states i s1' s2 ->
       t = E0 \/ output_trace t ->
       fbs_match i s1 (t, s2).
 
@@ -1655,18 +1671,18 @@ Lemma fbs_simulation:
   forall s2 t s2', Step (atomic L2) s2 t s2' ->
   forall i s1, fbs_match i s1 s2 -> safe L1 s1 ->
   exists i', exists s1',
-     (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order sim i' i))
+     (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ order i' i))
      /\ fbs_match i' s1' s2'.
 Proof.
   induction 1; intros.
-(* silent step *)
+- (* silent step *)
   inv H0.
   exploit (bsim_simulation sim); eauto. eapply star_safe; eauto.
   intros [i' [s1'' [A B]]].
   exists i'; exists s1''; split.
   destruct A as [P | [P Q]]. left. eapply star_plus_trans; eauto. right; split; auto. eapply star_trans; eauto.
   econstructor. apply star_refl. auto. auto.
-(* start step *)
+- (* start step *)
   inv H0.
   exploit (bsim_simulation sim); eauto. eapply star_safe; eauto.
   intros [i' [s1'' [A B]]].
@@ -1677,7 +1693,7 @@ Proof.
   left; auto.
   econstructor; eauto.
   exploit L2wb; eauto.
-(* continue step *)
+- (* continue step *)
   inv H0. unfold E0 in H8; destruct H8; try congruence.
   exploit star_non_E0_split'; eauto. simpl. intros [s1x [P Q]].
   exists i; exists s1x; split. left; auto. econstructor; eauto. simpl in H0; tauto.
@@ -1690,47 +1706,51 @@ Lemma fbs_progress:
   (exists t, exists s2', Step (atomic L2) s2 t s2').
 Proof.
   intros. inv H. destruct t.
-(* 1. no buffered events *)
+- (* 1. no buffered events *)
   exploit (bsim_progress sim); eauto. eapply star_safe; eauto.
   intros [[r A] | [t [s2' A]]].
-(* final state *)
++ (* final state *)
   left; exists r; simpl; auto.
-(* L2 can step *)
++ (* L2 can step *)
   destruct t.
   right; exists E0; exists (nil, s2'). constructor. auto.
   right; exists (e :: nil); exists (t, s2'). constructor. auto.
-(* 2. some buffered events *)
+- (* 2. some buffered events *)
   unfold E0 in H3; destruct H3. congruence.
   right; exists (e :: nil); exists (t, s3). constructor. auto.
 Qed.
 
+End FACTOR_BACKWARD_SIMULATION.
+
 Theorem factor_backward_simulation:
+  forall L1 L2,
+  backward_simulation L1 L2 -> single_events L1 -> well_behaved_traces L2 ->
   backward_simulation L1 (atomic L2).
 Proof.
-  apply Backward_simulation with (bsim_match_states := fbs_match) (bsim_order := bsim_order sim).
-(* wf *)
-  apply bsim_order_wf.
-(* initial states exist *)
+  intros L1 L2 BS L1single L2wb. 
+  destruct BS as [index order match_states sim].
+  apply Backward_simulation with order (fbs_match L1 L2 match_states); constructor.
+- (* wf *)
+  eapply bsim_order_wf; eauto.
+- (* initial states exist *)
   intros. exploit (bsim_initial_states_exist sim); eauto. intros [s2 A].
   exists (E0, s2). simpl; auto.
-(* initial states match *)
+- (* initial states match *)
   intros. destruct s2 as [t s2]; simpl in H0; destruct H0; subst.
   exploit (bsim_match_initial_states sim); eauto. intros [i [s1' [A B]]].
   exists i; exists s1'; split. auto. econstructor. apply star_refl. auto. auto.
-(* final states match *)
+- (* final states match *)
   intros. destruct s2 as [t s2]; simpl in H1; destruct H1; subst.
   inv H. exploit (bsim_match_final_states sim); eauto. eapply star_safe; eauto.
   intros [s1'' [A B]]. exists s1''; split; auto. eapply star_trans; eauto.
-(* progress *)
-  exact fbs_progress.
-(* simulation *)
-  exact fbs_simulation.
-(* symbols *)
+- (* progress *)
+  eapply fbs_progress; eauto.
+- (* simulation *)
+  eapply fbs_simulation; eauto.
+- (* symbols *)
   simpl. exact (bsim_public_preserved sim).
 Qed.
 
-End FACTOR_BACKWARD_SIMULATION.
-
 (** Receptiveness of [atomic L]. *)
 
 Record strongly_receptive (L: semantics) : Prop :=