proposition: Theorem unionStatePunionState : forall S1 S2 : State, unionStateP S1 S2 (unionState S1 S2).
proof: Proof. intros S1; elim S1; simpl in |- *; auto with stalmarck. intros S2. apply unionStatePSym; auto with stalmarck. apply unionStatePInclSelf; auto with stalmarck. apply inclStateIn; simpl in |- *; auto with stalmarck. intros a b H'; elim H'; auto with stalmarck. intros p l H' S2; case p; intros a b. apply unionStatePAssoc2 with (S1 := (a, b) :: nil) (S2 := l) (S'1 := unionState l S2); auto with stalmarck. generalize addEqUnion; unfold addEq in |- *; auto with stalmarck. generalize addEqUnion; unfold addEq in |- *; auto with stalmarck. Qed.
imports: Coq(List)