proposition: Lemma refine_opt2_fold_right' base ls new_comp old_comp (H : forall base base', refine base' base -> refine (x0 <- new_comp base; r_o x0) retv -> refine (x0 <- old_comp base'; r_o x0) retv) : make_tower base ls new_comp old_comp.
proof: Proof. revert base new_comp old_comp H; induction ls as [|x xs IHxs]; simpl; intros. { eapply H; [ | eassumption ]. reflexivity. } { destruct (proj x); simpl; intros; apply IHxs; clear IHxs; try intros ?? H'; apply H; edestruct test; specialize_by (exact eq_refl); simpl; try setoid_rewrite_hyp'; reflexivity. } Qed.
imports: Coq.Strings.String Fiat.Common.List.ListFacts Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.ADT.ComputationalADT Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements.HoneRepresentation Fiat.Parsers.ParserADTSpecification Fiat.Parsers.Refinement.IndexedAndAtMostOneNonTerminalReflective Fiat.Parsers.StringLike.Core Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations