proposition: Lemma map2_wd : forall F l H H' x, member x (map2 F l H) -> member x (map2 F l H').
proof: Proof. intros. rename X into H0. induction l as [| a l Hrecl]. simpl in |- *; simpl in H0; assumption. simpl in H0; inversion_clear H0. rename X into H0. simpl in |- *; left. apply Hrecl with (fun (y : IR) (H0 : member y l) => H y (@inl (member y l) (y [=] a) H0)). assumption. right. eapply eq_transitive_unfolded. apply H1. simpl in |- *; apply pfwdef; algebra. Qed.
imports: CoRN.reals.CReals1