proposition: Lemma incrMaxFreshIdx_computes: forall {qs_schema} {qidx: Fin.t (numRawQSschemaSchemas qs_schema)} (r: UnConstrQueryStructure qs_schema) l l', map indexedElement l' = l /\ (forall x : IndexedElement, In IndexedElement (GetUnConstrRelation r qidx) x <-> List.In x l') /\ NoDup (map elementIndex l') -> computes_to {idx: nat | UnConstrFreshIdx (GetUnConstrRelation r qidx) idx} (incrMaxFreshIdx l').
proof: Proof. intros qsc qidx r l l' [Hmap [Heqv Hdup]]. computes_to_econstructor. red; intros elem Helem. apply Heqv in Helem. unfold lt. apply le_n_S. apply fold_right_max_is_max. apply Helem. Qed.
imports: Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Bedrock.Word Coq.Arith.Arith Coq.Lists.List Fiat.QueryStructure.Automation.MasterPlan IndexedEnsembles Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTables Fiat.Narcissus.Examples.Guard.PacketFiltersLemmas Fiat.Narcissus.Examples.Guard.DropFields Coq.Sets.Ensembles