proposition: Lemma cConstructors_AbsR {Sig} {spec : ADT Sig} (impl : FullySharpened spec) midx : @Lift_Constructor2P _ _ _ (fun Cons cCons => exists r_o', computes_to Cons (r_o') /\ AbsR (projT2 impl) r_o' cCons) (Constructors spec midx) (cConstructors (projT1 impl) midx).
proof: Proof. simpl in *. generalize (ADTRefinementPreservesConstructors (projT2 impl) midx). intro. eapply Lift_Constructor2P_ind with (P' := fun dom meth (cCons : cConstructorType _ dom) => refineConstructor (AbsR (projT2 impl)) meth (LiftcConstructor _ dom cCons)) ; simpl; intros; eauto. - revert H0; clear -midx; destruct (ConstructorDom Sig midx) as [|]; simpl; intros; specialize (H0 _ (ReturnComputes _)); computes_to_inv; subst; eexists; split; simpl; try destruct v; simpl; 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