proposition: Lemma compare : forall c1 c2 : Channel, {c1 = c2} + {c1 <> c2}.
proof: Proof. simple destruct c1. simple destruct c2. left; try trivial. right; red in |- *; intros H; discriminate H. right; red in |- *; intros H; discriminate H. simple destruct c2. right; red in |- *; intros H; discriminate H. left; trivial. right; red in |- *; intros H; discriminate H. simple destruct c2. right; red in |- *; intros H; discriminate H. right; red in |- *; intros H; discriminate H. left; trivial. Defined.
imports: ABP.ABP.BISIMULATION.Protocol