proposition: Lemma map2_pres_member : forall (F : PartIR) x Hx l H, member x l -> member (F x Hx) (map2 F l H).
proof: Proof. intros. rename X into H0. induction l as [| a l Hrecl]. simpl in |- *; simpl in H; assumption. simpl in |- *. elim H0. intro; left; apply Hrecl; assumption. intro; right. apply pfwdef; assumption. Qed.
imports: CoRN.reals.CReals1