proposition: Lemma RealElemToElem_inj : forall idx, Injective (@RealElemToElem idx).
proof: Proof. unfold RealElemToElem, Injective. eauto using TupleToListW_inj. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.FacadeLoops CertifiedExtraction.Extraction.External.Lists CertifiedExtraction.Extraction.QueryStructures.CallRules.Tuple