proposition: Theorem doTripletsExTrace : forall (L : list triplet) (S1 S2 : State), doTripletsP S1 L S2 -> exists t : Trace, evalTrace S1 t S2 /\ TraceInList t L.
proof: Proof. intros L S1 S2 H'; elim H'; clear H' S1 S2 L. intros S1 S2 H' H'0; exists emptyTrace; simpl in |- *; auto with stalmarck. intros S1 S2 S3 L t H' H'0 H'1 H'2; elim H'2; intros t0 E; elim E; intros H'3 H'4; clear E H'2. exists (seqTrace (tripletTrace t) t0); simpl in |- *; repeat split; auto with stalmarck. apply seqTraceEval with (S2 := S2); auto with stalmarck. apply tripletTraceEval with (S2 := S2); auto with stalmarck. Qed.