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