proposition: Lemma nat__fin : forall (n : nat) (i : fin n), nat_to_fin (fin_to_nat i) (fin_lt_n n i) = i.
proof: Proof. intros. funelim (fin_to_nat i); simpl. reflexivity. f_equal. rewrite <- H at 4. f_equal. apply le_hprop. Qed.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations