proposition: Lemma mu'_complete n0 : P (ext n0) == ext true -> (forall n', n' < n0 -> P (ext n') == ext false) -> mu' P (ext 0) == ext n0.
proof: Proof. Proof using P_proc. intros. rewrite mu'_0_false with (n:=n0);try tauto. - recStep mu'. Lsimpl. rewrite H. unfold K. now Lsimpl. Qed.