+(* Obviously, broadcasting does not change the carrier of the item,
+as it is easily proved by structural induction. *)
+
+lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
+#S #i elim i //
+ [ #i1 #i2 #IH1 #IH2 >erase_dot <IH1 >eclose_dot
+ cases (•i1) #i11 #b1 cases b1 // <IH2 >odot_true_bis //
+ | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) <IH1 <IH2
+ cases (•i1) #i11 #b1 cases (•i2) #i21 #b2 //
+ | #i #IH >eclose_star >(erase_star … i) <IH cases (•i) //
+ ]
+qed.
+
+(* We are now ready to state the main semantic properties of $\oplus,
+\triangleleft$ and $\bullet(-)$:
+
+\begin{lstlisting}[language=grafite]
+lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
+ \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
+lemma sem_pcl : ∀S.∀e1:pre S.∀i2:pitem S.
+ \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+theorem sem_bullet: ∀S:DeqSet. ∀i:pitem S.
+ \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
+\end{lstlisting}
+The proof of \verb+sem_oplus+ is straightforward. *)
+