proposition: Lemma MostlySharpened_Start : forall {Sig} (spec : ADT Sig) adt cadt, (@refineADT _ spec adt) -> (@FullySharpenedUnderDelegates _ adt cadt) -> MostlySharpened spec.
proof: Proof. intros; exists (adt, cadt); eauto. Defined.
imports: Coq.Lists.List Coq.Strings.String Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.ADT.Core Fiat.ADT.ComputationalADT Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms