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) -> nth_error (TupleToListW tup) (` (Fin.to_nat idx)) = Some (match CompileGet_helper idx in (_ = W) return (Vector.nth (MakeVectorOfW N) idx -> W) with | eq_refl => fun t : Vector.nth (MakeVectorOfW N) idx => t end (ilist2.ith2 tup idx)).
proof: Proof. intros. induction idx; simpl. - reflexivity. - destruct (Fin.to_nat idx); simpl. rewrite IHidx. + reflexivity. + apply BinNat.N.lt_succ_l. rewrite Nnat.Nat2N.inj_succ in H; assumption. Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core