proposition: Lemma Sharpened_encode_SensorData_Impl : { encode_SensorData_Impl : _ & forall ce (val : SensorType), refine (encode_SensorData_Spec val ce) (ret (encode_SensorData_Impl val ce))}.
proof: Proof. eexists; intros; set_evars. unfold encode_SensorData_Spec. unfold compose, Bind2. setoid_rewrite refine_encode_enum; simplify with monad laws. setoid_rewrite (@refine_encode_SumType bin _ 2 ([nat : Type; nat : Type]) _ (icons _ (icons _ (inil (A := Type))))). simplify with monad laws. simpl; rewrite app_nil_r. finish honing. simpl; f_equiv. simpl; repeat apply Build_prim_and; eauto; intros; rewrite refine_encode_nat; finish honing. Defined.
imports: Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Coq.Structures.OrderedType Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Compose Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Lib2.WordOpt Fiat.Narcissus.Lib2.NatOpt Fiat.Narcissus.Lib2.StringOpt Fiat.Narcissus.Lib2.EnumOpt Fiat.Narcissus.Lib2.FixListOpt Fiat.Narcissus.Lib2.SumTypeOpt Fiat.Common.SumType Fiat.Examples.Tutorial.Tutorial Fiat.Examples.DnsServer.DecomposeEnumField Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.MasterPlan Fiat.Examples.HACMSDemo.DuplicateFree Fiat.Examples.HACMSDemo.HACMSDemo Fiat.Examples.HACMSDemo.WheelSensor