proposition: Lemma CompileGet_goodSize_helper: forall (N : nat) (idx : Fin.t N), BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> IL.goodSize (` (Fin.to_nat idx)).
proof: Proof. intros *. pose proof (proj2_sig (Fin.to_nat idx)) as h; simpl in h. apply NPeano.Nat.le_exists_sub in h; repeat cleanup. assert (IL.goodSize N) as h. eassumption. rewrite H0 in h. eapply Arrays.goodSize_plus_r. rewrite NPeano.Nat.add_succ_r in h. rewrite <- NPeano.Nat.add_succ_l in h. eassumption. Defined.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core