proposition: Lemma restrict_injective n f h : Injective (@restrict n f h) <-> bInjective n f.
proof: Proof. split. - intros hf x y hx hy Eq. rewrite <- (f2n_n2f hx), <- (f2n_n2f hy). f_equal. apply hf. rewrite 2 restrict_n2f. generalize (h x hx) (h y hy). rewrite Eq. apply n2f_ext. - intros hf x y Eq. apply f2n_inj. apply hf; try apply f2n_ok. now rewrite <- 2 (restrict_f2n h), Eq. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec