proposition: Lemma inj_Tmess : forall (c1 : Channel) (v1 v2 : Act c1) (p1 p2 : Process) (c3 c4 : Channel) (f1 : Act c3 -> Process) (f2 : Act c4 -> Process), ACTALK Channel Act c1 v1 p1 c3 f1 = ACTALK Channel Act c1 v2 p2 c4 f2 -> v1 = v2.
proof: Proof. simple destruct c1. intros v1 v2 p1 p2 c3 c4 f1 f2 H. apply (disc_mess (ACTALK Channel Act lnk1 v1 p1 c3 f1) (ACTALK Channel Act lnk1 v2 p2 c4 f2) H lnk1 v1). intros v1 v2 p1 p2 c3 c4 f1 f2 H. apply (disc_mess (ACTALK Channel Act lnk2 v1 p1 c3 f1) (ACTALK Channel Act lnk2 v2 p2 c4 f2) H lnk2 v1). intros v1 v2 p1 p2 c3 c4 f1 f2 H. apply (disc_mess (ACTALK Channel Act del v1 p1 c3 f1) (ACTALK Channel Act del v2 p2 c4 f2) H del v1). Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses