proposition: Lemma decode_encode_fin `{Finite A} (x : A) : decode_fin (encode_fin x) = x.
proof: Proof. unfold decode_fin, encode_fin. destruct (Some_dec _) as [[x' Hx]|Hx]. { by rewrite fin_to_nat_to_fin, decode_encode_nat in Hx; simplify_eq. } exfalso; by rewrite ->fin_to_nat_to_fin, decode_encode_nat in Hx. Qed.
imports: stdpp(options)