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