proposition: Lemma CompileGet_helper': forall (N : nat) (tup : FiatTuple N) (idx : Fin.t N), BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> Word.wlt (Word.natToWord 32 (` (Fin.to_nat idx))) (IL.natToW (Datatypes.length (TupleToListW tup))).
proof: Proof. intros. rewrite TupleToListW_length by assumption. pose proof (proj2_sig (Fin.to_nat idx)) as h; simpl in h. apply Arrays.lt_goodSize; try eassumption. apply CompileGet_goodSize_helper; assumption. Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core