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