proposition: Lemma Relabel_Realise R : pM ⊨ R -> Relabel ⊨ ⋃_y (R |_ y) ||_(p y).
proof: Proof. intros HRel. intros tin k outc HLoop. hnf in HRel. specialize HRel with (1 := HLoop). hnf. now exists (projT2 pM (cstate outc)). Qed.