proposition: Lemma SEND_UinvR : forall (P : bool -> Process -> bool -> Stream A -> Prop) (v : bool) (q : Process) (b : bool) (s : Stream A), P v (SEND b s) b s -> UnrelProcTrans Channel Act lnk2 (SEND b s) (Receive _ Act lnk2 v) q -> P v q b s.
proof: Proof. intros P b1 q b s H. rewrite unfold_SEND. intros H0. simple inversion H0. discriminate H2. rewrite <- H3. rewrite (inj_Tfun c1 lnk1 v1 (b, hd s) p1 (SENDING b s) lnk2 f (fun b1 : bool => SEND b s)). assumption. assumption. intro. absurd (c2 = lnk2). assumption. injection H2; trivial. discriminate H2. discriminate H2. discriminate H2. discriminate H3. discriminate H3. discriminate H3. discriminate H3. discriminate H3. Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses