proposition: Lemma FullySharpened_Finish : forall {Sig} (spec : ADT Sig) adt (cadt : ComputationalADT.cADT Sig), @FullySharpenedUnderDelegates _ spec adt -> forall (DelegateReps : Fin.t (Sharpened_DelegateIDs adt) -> Type) (DelegateImpls : forall idx, ComputationalADT.pcADT (Sharpened_DelegateSigs adt idx) (DelegateReps idx)) (ValidImpls : forall idx : Fin.t (Sharpened_DelegateIDs adt), refineADT (Sharpened_DelegateSpecs adt idx) (ComputationalADT.LiftcADT (existT _ _ (DelegateImpls idx)))), refineADT (ComputationalADT.LiftcADT (Sharpened_Implementation adt DelegateReps DelegateImpls)) (ComputationalADT.LiftcADT cadt) -> refineADT spec (ComputationalADT.LiftcADT cadt).
proof: Proof. intros. eapply transitivityT; eauto. Qed.
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