proposition: Lemma CompileGet_helper : forall N (idx: (Fin.t N)), (@Vector.nth Type (NumAttr (MakeWordHeading N)) (AttrList (MakeWordHeading N)) idx) = W.
proof: Proof. induction idx; eauto. Defined.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core