proposition: Lemma linear_search_rel : forall start b, rel_ls start (prog_linear_search start b).
proof: Proof. intros start b. induction b as [n p | n b IHb] using before_witness_dep_ind; unfold prog_linear_search; destruct (P_dec n) as [yes | no]; fold prog_linear_search. - apply Rstop, yes. - case (no p). - apply Rstop, yes. - apply (Rnext no), IHb. Qed.
imports: Arith