proposition: Lemma FiatTupleToBedrockTuple_length : forall {N} (v: FiatTuple N), List.length (FiatTupleToBedrockTuple v) = N.
proof: Proof. intros. unfold FiatTupleToBedrockTuple. apply TupleToListW_length. Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core