proposition: Theorem restrictDoTripletsCompAux1 : forall (S1 S2 : State) (L : list triplet), doTripletsP S1 L S2 -> forall S3 : State, eqState S1 (restrictState S3 (ResTriplets L)) -> eqState S2 (restrictState S2 (ResTriplets L)).
proof: Proof. intros S1 S2 L H'; Elimc H'; clear L S1 S2; auto with stalmarck. intros S1 S2 L H' S3 H'0. apply eqStateTrans with (S2 := S1); auto with stalmarck. apply eqStateTrans with (S2 := restrictState S3 (ResTriplets L)); auto with stalmarck. apply eqStateTrans with (S2 := restrictState (restrictState S3 (ResTriplets L)) (ResTriplets L)); auto with stalmarck. apply restrictStateInvol; auto with stalmarck. apply restrictEqComp; auto with stalmarck. apply eqStateTrans with (S2 := S1); auto with stalmarck. intros S1 S2 S3 L t H' H'0 H'1 H'2 S0 H'3. elim (doTripletEqCompEx S1 S2 (restrictState S0 (ResTriplets L)) t); [ intros S4 E; Elimc E; intros H'10 H'11 | idtac | idtac ]; auto with stalmarck. apply (H'2 S2); auto with stalmarck. apply eqStateTrans with (S2 := S4); auto with stalmarck. apply eqStateTrans with (S2 := restrictState S4 (ResTriplets L)); auto with stalmarck. apply restrictDoTripletComp with (S1 := S0) (t := t); auto with stalmarck. apply ResTripletInResTriplets; auto with stalmarck. apply restrictEqComp; auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)