proposition: Lemma DropPreservesFreshIdx: forall h r_o (r_n: UnConstrQueryStructure (PacketHistorySchema h)) totup, Complete_Dropped_qs_equiv totup r_o r_n -> refine {idx: nat | UnConstrFreshIdx (GetUnConstrRelation r_o Fin.F1) idx} {idx: nat | UnConstrFreshIdx (GetUnConstrRelation r_n Fin.F1) idx}.
proof: Proof. intros h r_o r_n totup H. red in H. intro v; intros Hv; computes_to_inv. red in Hv. computes_to_econstructor. red; intros [idx [inp tmp]] Hinp. cbn in inp; destruct tmp. apply (H inp idx) in Hinp. apply Hv in Hinp. cbn in *. assumption. Qed.
imports: Bedrock.Word Coq.Vectors.Vector IndexedEnsembles Fiat.Common.ilist2 Fiat.Common.EnumType Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTables IPTables