proposition: Lemma Evt3 : forall (b : bool) (s : Stream A) (p : Process) (ss : Discourse Channel Act), Equity p ss -> p = SENDING b s || OUT b (hd s) -> Evt Channel Act Trans (OneDel (hd s)) p ss.
proof: Proof. intros b s p ss H. elim (Evt_from_Equity p ss H). intros q c w ss0 p0 T H1 HypInd whichisp0. apply (notyet _ _ Trans (OneDel (hd s)) q). assumption. intros q0 T0 H0. rewrite whichisp0 in T0. case (State3 b s c w q0). assumption. intros state3. case state3. intros whichisc whichisq0. apply HypInd. rewrite whichisp0; assumption. unfold Precondition in |- *. red in |- *. intro. apply H2. rewrite whichisp0. apply exep3. assumption. assumption. intros state4. case state4. intros whichiscw whichisq0. case H0. unfold OneDel in |- *. assumption. Defined.
imports: ABP.ABP.TRACES.Lemmas