proposition: Theorem evalTraceEq : forall (S1 S2 : State) (t : Trace), evalTrace S1 t S2 -> forall S3 S4 : State, evalTrace S3 t S4 -> eqState S1 S3 -> eqState S2 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; inversion H'0; auto with stalmarck. intros H'1. apply eqStateTrans with (S2 := S1); auto with stalmarck. apply eqStateTrans with (S2 := S3); auto with stalmarck. intros t S1 S2 S3 H' H'0 S4 S5 H'1 H'2; inversion H'1; auto with stalmarck. apply eqStateTrans with (S2 := S2); auto with stalmarck. apply eqStateTrans with (S2 := S6); auto with stalmarck. apply doTripletEqComp with (t := t) (S1 := S1) (S2 := S4); auto with stalmarck. intros t1 t2 S1 S2 S3 H' H'0 H'1 H'2 S0 S4 H'3; inversion H'3; auto with stalmarck. intros H'4. apply (H'2 S6); auto with stalmarck. apply H'0 with (S3 := S0); auto with stalmarck. intros t1 t2 a b S1 S2 S3 S4 H' H'0 H'1 H'2 H'3 S0 S5 H'4; inversion H'4; auto with stalmarck. intros H'5. apply eqStateTrans with (S2 := interState S7 S8); auto with stalmarck. apply eqStateTrans with (S2 := interState S2 S3); auto with stalmarck. apply interStateEq; auto with stalmarck. apply H'0 with (S3 := addEq (a, b) S0); auto with stalmarck. apply (H'2 (addEq (a, rZComp b) S0)); auto with stalmarck. Qed.