proposition: Theorem doTripletCongruent : forall (S1 S2 S3 : State) (L : list triplet), doTripletsP S1 L S2 -> doTripletsP (unionState S3 S1) L (unionState S3 S2).
proof: Proof. intros S1 S2 S3 L H'; Elimc H'; clear S1 S2 L; auto with stalmarck. intros S1 S2 S0 L t H' H'0 H'1 H'2. apply doTripletsRTrans with (S2 := unionState S3 S2); auto with stalmarck. elim (doTripletCongruentEx S1 S2 S3 t); [ intros S4 E; Elimc E; intros H'8 H'9 | idtac ]; auto with stalmarck. apply doTripletsRTrans with (S2 := S4); auto with stalmarck. apply doTripletsTrans with (S2 := S4) (t := t); auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux)