map2_nonexpanding' `{!NonExpanding f} `{!NonExpanding g} : NonExpanding (map2 f g). Proof. intros e u v xi;split;simpl; apply (non_expanding _),xi. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.