proposition: Lemma MakeWordHeading_allWords : forall {N} (idx: Fin.t N), Domain (MakeWordHeading N) idx = W.
proof: Proof. unfold MakeWordHeading; induction idx. - reflexivity. - unfold Domain in *; simpl in *; assumption. Defined.
imports: Fiat.Computation.Notations Fiat.ADT.Core Fiat.Computation.Core Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory