fact: Axiom FiatTupleToBedrockTuple_length : forall {N} (v: FiatTuple N), List.length (FiatTupleToBedrockTuple v) = N.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core