proposition: Lemma listen : forall (p : Process Chnl A) (c : Chnl) (v : A c), {q : Process Chnl A | UnrelProcTrans Chnl A c p (Receive _ _ c v) q}.
proof: Proof. fix 1. simple destruct p. simple destruct g. intros c1 a0 p0 c2 f c0. case (compare c2 c0). intros H. pattern c0 in |- *. case H. intros. exists (INJ Chnl A (f v)). apply uttalk2. trivial. intros. exists (INJ Chnl A (TALK Chnl A c1 a0 p0 c2 f)). apply uttalk3. assumption. intros c p0 c0. case (compare c c0). intros H. pattern c0 in |- *. case H. intros. exists (INJ Chnl A (p0 v)). apply utlisten1. trivial. intros. exists (INJ Chnl A (LISTEN Chnl A c p0)). apply utlisten2. assumption. intros. case (listen p0 c v). intros. case (listen p1 c v). intros. exists (PAR Chnl A x x0). apply utpar3. assumption. assumption. Defined.
imports: ABP.INTERPRETER.Processes