proposition: Lemma SEND_UinvTC1 : forall (P : bool * A -> Process -> bool -> Stream A -> Prop) (v : bool * A) (q : Process) (b : bool) (s : Stream A), P (b, hd s) (SENDING b s) b s -> UnrelProcTrans Channel Act lnk1 (SEND b s) (Transmit _ Act lnk1 (Clear _ Act lnk1 v)) q -> P v q b s.
proof: Proof. intros P v q b s H. rewrite (unfold_SEND b s). intros H2. simple inversion H2. injection H1 as <-. rewrite (inj_Tmess lnk1 v0 (b, hd s) p (SENDING b s) c2 lnk2 f (fun b1 : bool => SEND b s)). rewrite <- H3. injection H0 as ? ->. assumption. assumption. discriminate H1. discriminate H3. discriminate H1. discriminate H3. discriminate H1. discriminate H3. discriminate H3. discriminate H3. discriminate H3. discriminate H3. Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses