proposition: Lemma FiatTupleToBedrockTuple_inj : forall {N} (v v' : FiatTuple N), FiatTupleToBedrockTuple v = FiatTupleToBedrockTuple v' -> v = v'.
proof: Proof. eauto using TupleToListW_inj. Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core