proposition: Lemma disc_mess : forall p1 p2 : Process, p1 = p2 -> forall (c : Channel) (a : Act c), select_mess p1 c a = select_mess p2 c a.
proof: Proof. intros p1 p2 H. rewrite H. trivial. Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses