proposition: Lemma inj_elts_subset P Q (h : P [<=] Q) : injective (elts_subset h).
proof: Proof. intros [x_val x] [y_val y] e. apply sig_eq in e. apply sig_eq. hyp. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(LogicUtil RelUtil FunUtil ListUtil NatUtil ClassicUtil BoundNat)