proposition: Lemma restrict_n2f n f hf x (h:x<n) : @restrict n f hf (n2f h) = n2f (hf _ h).
proof: Proof. unfold restrict. generalize (f2n_n2f h). unfold f2n. destruct (Fin.to_nat (n2f h)) as (x',h'); simpl. intros ->. now apply n2f_ext. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec