proposition: Theorem stalmarckComp : forall (S1 S2 S3 S4 : State) (L : list triplet), stalmarckP S1 L S2 -> eqState S3 S1 -> eqState S4 S2 -> stalmarckP S3 L S4.
proof: Proof. intros S1 S2 S3 S4 L H'; generalize S3 S4; Elimc H'; clear L S1 S2 S3 S4. intros S1 S2 L H' S3 S4 H'0 H'1. apply stalmarckPref; auto with stalmarck. apply doTripletsComp with (1 := H'); auto with stalmarck. intros a b S1 S2 S3 S4 L H' H'0 H'1 H'2 H'3 S5 S6 H'4 H'5. apply stalmarckPSplit with (a := a) (b := b) (S2 := S2) (S3 := S3); auto with stalmarck. apply eqStateTrans with (S2 := S4); auto with stalmarck. intros S1 S2 S3 L H' H'0 H'1 H'2 S4 S5 H'3 H'4. apply stalmarckTrans with (S2 := S2); auto with stalmarck. Qed.