proposition: Lemma SENDING_SinvR : forall (P : A -> Process -> bool -> Stream A -> Prop) (v : A) (q : Process) (b : bool) (s : Stream A), P v (SENDING b s) b s -> SafeProcTrans Channel Act del (SENDING b s) (Receive Channel Act del v) q -> P v q b s.
proof: Proof. intros P v q b s H. rewrite unfold_SENDING. intros H1. simple inversion H1. discriminate H2. discriminate H2. rewrite <- H4. rewrite H2. rewrite <- (unfold_SENDING b s). auto. discriminate H2. discriminate H2. discriminate H3. discriminate H3. discriminate H3. Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses