proposition: Theorem evalTraceEq : forall (S1 S2 S3 S4 : State) (T : Trace), evalTrace S1 T S2 -> eqState S1 S3 -> eqState S2 S4 -> evalTrace S3 T S4.
proof: Proof. intros S1 S2 S3 S4 T H'; generalize S3 S4; clear S3 S4; elim H'; auto with stalmarck. intros S3 S4 H'0 S5 S6 H'1 H'2. apply emptyTraceEval; auto with stalmarck. apply eqStateTrans with S3; auto with stalmarck. apply eqStateTrans with S4; auto with stalmarck. intros t S3 S4 S5 H'0 H'1 S6 S7 H'2 H'3. apply evalTraceComp with (S1 := S3) (S2 := S5); auto with stalmarck. apply tripletTraceEval with (S2 := S4); auto with stalmarck. intros t1 t2 S3 S4 S5 H'0 H'1 H'2 H'3 S6 S7 H'4 H'5. apply seqTraceEval with (S2 := S4); auto with stalmarck; auto with stalmarck. intros t1 t2 a b S3 S4 S5 S6 H'0 H'1 H'2 H'3 H'4 S7 S8 H'5 H'6. apply dilemmaTraceEval with (S2 := S4) (S3 := S5); auto with stalmarck. apply eqStateTrans with S6; auto with stalmarck. Qed.