well_ord_iso_predE replaces not_well_ord_iso_pred
well_ord_iso_unique: eliminated a premise using well_ord_ord_iso
Proved well_ord_iso_pred_eq, ord_iso_image_pred, ord_iso_restrict_pred,
part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso, well_ord_ord_iso,
well_ord_iso_preserving, mono_map_is_fun, mono_map_is_inj, mono_map_trans,
mono_ord_isoI, well_ord_mono_ord_isoI, ord_iso_is_mono_map,
ord_iso_map_mono_map, ord_iso_map_ord_iso, domain_ord_iso_map_subset,
domain_ord_iso_map_cases, range_ord_iso_map_cases, well_ord_trichotomy
deleted bij_ss in favour of bij_inverse_ss
#! /bin/sh
# teeinput -- start a program and log all inputs to a file
# environment variable $LISTEN specifies the file name
tee -a -i $LISTEN | $*