proposition: Lemma FiatBagToBedrockBag_inj : forall {N}, Injective (@FiatBagToBedrockBag N).
proof: Proof. red; intros; apply IndexedEnsemble_TupleToListW_inj; assumption. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core