proposition: Lemma takeUntil_wd {A B} {P : Stream A → bool} {s:Stream A} (ex1 ex2 : LazyExists (fun x => Is_true (P x)) s) (cons : A → B → B) (nil : B) : takeUntil P ex1 cons nil ≡ takeUntil P ex2 cons nil.
proof: Proof. assert (H:=ex1). induction H; case ex1; clear ex1; case ex2; clear ex2; simpl; destruct (P x); try contradiction; auto. intros ex2 ex1. rewrite (H0 tt (ex1 tt) (ex2 tt)). reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax Coq.QArith.QArith Coq.Bool.Bool CoRN.metric2.Complete MathClasses.theory.CoqStreams MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.orders.naturals