proposition: Theorem doTripletsTermEx : forall (L : list triplet) (S1 S2 : State), doTripletsP S1 L S2 -> eqState S1 S2 \/ (exists t : triplet, (exists S3 : State, In t L /\ doTripletP S1 t S3 /\ doTripletsP S3 (rem _ tripletDec t L) S2)).
proof: Proof. intros L S1 S2 H'; inversion H'; auto with stalmarck. right; exists t; exists S3; split; try split; auto with stalmarck. lapply (doTripletsTermExAux L S3 S2); [ intros H'3; elim (H'3 t); [ intros H'6 | intros H'6; Elimc H'6; intros S5 E; Elimc E; intros S6 E; Elimc E; intros H'6 H'7; Elimc H'7; intros H'7 H'8 | idtac ] | idtac ]; auto with stalmarck. apply doTripletsRTrans with (S2 := S5); auto with stalmarck. apply doTripletsComp with (S1 := S6) (S2 := S2); auto with stalmarck. apply doTripletInvol with (t := t) (S1 := S1) (S2 := S3); auto with stalmarck. apply doTripletsIncl with (L := rem triplet tripletDec t L); auto with stalmarck. Qed.
imports: Stalmarck(PolyListAux)