proposition: Lemma ACK_UinvR : forall (P : bool * A -> Process -> bool -> Prop) (v : bool * A) (q : Process) (b : bool), P v (ACK b) b -> UnrelProcTrans Channel Act lnk1 (ACK b) (Receive _ Act lnk1 v) q -> P v q b.
proof: Proof. intros P v q b H. rewrite unfold_ACK. intros H0. simple inversion H0. discriminate H2. rewrite <- H3. rewrite (inj_Tfun c1 lnk2 v1 b p1 (ACKING b) lnk1 f (fun _ : bool * A => ACK b)) . 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