proposition: Lemma ValidUpdateCorrect : forall (A : Prop), false = true -> A.
proof: Proof. intros; discriminate. Qed.
imports: Coq.Strings.String Fiat.ADTRefinement.GeneralBuildADTTactics Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsOfTuples Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Automation.AutoDB Fiat.Common.ilist3_pair Fiat.Common.ilist3 Fiat.Common.i3list2