proposition: Lemma extend_f2n n f (x:Fin.t n) : extend f (f2n x) = f2n (f x).
proof: Proof. generalize (n2f_f2n x). unfold extend, f2n, f2n_ok. destruct (Fin.to_nat x) as (x',h); simpl. break_dec h. now intros ->. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec