proposition: Lemma BinNat_lt_Fin_to_nat: forall (N : nat) (idx : Fin.t N), BinNat.N.lt (BinNat.N.of_nat (projT1 (Fin.to_nat idx))) (BinNat.N.of_nat N).
proof: Proof. intros. pose proof (projT2 (Fin.to_nat idx)). Nomega.nomega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Memory