proposition: Theorem doTripletRestrictAux1 : forall (S : State) (t : triplet) (L : list rNat) (p1 q1 p q r s : rZ), eqStateRz S p1 q1 -> eqStateRz (restrictState S L) p1 q1 -> In (valRz p) L -> In (valRz q) L -> In (valRz r) L -> In (valRz s) L -> In zero L -> (eqStateRz (restrictState S L) p1 q1 -> doTripletP (restrictState S L) t (addEq (p, q) (addEq (r, s) (restrictState S L)))) -> ex (fun S' : State => doTripletP (restrictState S L) t S' /\ eqState (restrictState (addEq (p, q) (addEq (r, s) S)) L) S').
proof: Proof. intros S t L p1 q1 p q r s H' H'0 H'1 H'2 H'3 H'4 H'5 H'6; exists (addEq (p, q) (addEq (r, s) (restrictState S L))); split; auto with stalmarck. apply eqStateTrans with (S2 := addEq (p, q) (restrictState (addEq (r, s) S) L)); auto with stalmarck. apply RestrictAddEq; auto with stalmarck. apply eqStateAddEq; auto with stalmarck. apply RestrictAddEq; auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)