proposition: Lemma make_tower_const base ls v v' (H : refine v' v) : make_tower base ls (fun _ => v) (fun _ => v').
proof: Proof. induction ls as [|x xs IHxs]; simpl. { rewrite H; intro; assumption. } { destruct (proj x); intros; assumption. } 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