proposition: Lemma Unique3 : forall (b : bool) (s : Stream A) (p : Process) (ss : Discourse Channel Act) (q : Process) (ss1 : Discourse Channel Act), Wittness Channel Act Trans A OneDel (hd s) q ss1 p ss -> p = SENDING b s || OUT b (hd s) -> q = SENDING b s || ACK b.
proof: Proof. intros b s p ss q ss1 H. elim H. intros p0 ss0 c0 w0 q0 T H1 H2 HypInd whichisp0. apply HypInd. case (State3 b s c0 w0 q0). rewrite whichisp0 in T; assumption. intro state3; case state3; auto. intro state3; case state3; intros whichc whichq0. unfold OneDel in H1. absurd (existS (Signal Channel Act) c0 w0 = existS (Signal Channel Act) del (Clear Channel Act del (hd s))); auto. intros c0 w0 p0 T H1 whichisp0. case (State3 b s c0 w0 q). rewrite whichisp0 in T; assumption. intro state3; case state3; intros whichc whichq0. absurd (c0 = lnk1). unfold OneDel in H1. dependent rewrite H1. discriminate. assumption. intro state3; case state3; auto. Defined.
imports: ABP.ABP.TRACES.Lemmas