proposition: Lemma restrict_f2n n f hf (x:Fin.t n) : f2n (@restrict n f hf x) = f (f2n x).
proof: Proof. unfold restrict, f2n. destruct (Fin.to_nat x) as (x',h); simpl. apply f2n_n2f. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec