proposition: Lemma mu'_0_false n: (forall n', n' < n -> P (ext n') == ext false) -> mu' P (ext 0) >* mu' P (ext n).
proof: Proof. Proof using P_proc. intros H. induction n. - reflexivity. - rewrite IHn. + apply mu'_n_false. apply H. lia. + intros. apply H. lia. Qed.