proposition: Lemma LessHistoryRelationRefl: forall h (totup: input -> @Tuple h) r_o, FiniteTables_AbsR r_o r_o -> LessHistoryRelation totup r_o r_o.
proof: Proof. unfold LessHistoryRelation; split. assumption. split; intros; assumption. 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