proposition: Lemma OUT_UinvR : forall (P : bool * A -> Process -> bool -> A -> Prop) (v : bool * A) (q : Process) (b : bool) (a : A), P v (OUT b a) b a -> UnrelProcTrans Channel Act lnk1 (OUT b a) (Receive _ Act lnk1 v) q -> P v q b a.
proof: Proof. intros P v q b a H. rewrite unfold_OUT. intro H0. simple inversion H0. discriminate H2. rewrite <- H3. rewrite (inj_Tfun c1 del v1 a p1 (ACK b) lnk1 f (fun _ : bool * A => OUT b a)) . assumption. assumption. intro. absurd (c2 = lnk1). 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