proposition: Lemma FullySharpened_Start : forall {Sig} (spec : ADT Sig) cadt, refineADT spec (LiftcADT cadt) -> FullySharpened spec.
proof: Proof. intros; exists cadt; eassumption. 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