proposition: Theorem doTripletsRTrans : forall (S1 S2 S3 : State) (L : list triplet), doTripletsP S1 L S2 -> doTripletsP S2 L S3 -> doTripletsP S1 L S3.
proof: Proof. intros S1 S2 S3 L H'; elim H'; auto with stalmarck. intros S4 S5 L0 H'0 H'1. apply doTripletsComp with (S1 := S5) (S2 := S3); auto with stalmarck. intros S4 S5 S0 L0 t H'0 H'1 H'2 H'3 H'4. apply doTripletsTrans with (S2 := S5) (t := t); auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux)