proposition: Theorem doTripletsComp : forall (S1 S2 S3 S4 : State) (L : list triplet), doTripletsP S1 L S2 -> eqState S3 S1 -> eqState S4 S2 -> doTripletsP S3 L S4.
proof: Proof. intros S1 S2 S3 S4 L H'; generalize S3 S4; elim H'; clear H' L S1 S2 S3 S4; auto with stalmarck. intros S1 S2 L H' S3 S4 H'0 H'1. apply doTripletsRef; auto with stalmarck. apply eqStateTrans with (S2 := S1); auto with stalmarck. apply eqStateTrans with (S2 := S2); auto with stalmarck. intros S1 S2 S3 L t H' H'0 H'1 H'2 S0 S4 H'3 H'4. elim (doTripletEqCompEx S1 S2 S0 t); [ intros S6 E; Elimc E; intros H'11 H'12 | idtac | idtac ]; auto with stalmarck. apply doTripletsTrans with (S2 := S6) (t := t); auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux)