proposition: Lemma inj_Lfun : forall (c3 : Channel) (f1 f2 : Act c3 -> Process), ACLISTEN Channel Act c3 f1 = ACLISTEN Channel Act c3 f2 -> f1 = f2.
proof: Proof. simple destruct c3. intros f1 f2 H. apply (disc_fun (ACLISTEN Channel Act lnk1 f1) (ACLISTEN Channel Act lnk1 f2) H lnk1). intros f1 f2 H. apply (disc_fun (ACLISTEN Channel Act lnk2 f1) (ACLISTEN Channel Act lnk2 f2) H lnk2). intros f1 f2 H. apply (disc_fun (ACLISTEN Channel Act del f1) (ACLISTEN Channel Act del f2) H del). Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses