proposition: Lemma StringBound_contra : @StringBound.BoundedString nil -> False.
proof: Proof. destruct 1 as [ ? [ [ ] ] ]; simpl in *; discriminate. Qed.
imports: Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildComputationalADT Fiat.ADTNotation.BuildADTSig Fiat.ADTRefinement.GeneralRefinements Fiat.Common.ilist Fiat.ADTRefinement.BuildADTRefinements.HoneRepresentation Fiat.ADT.ComputationalADT Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.ADT.ComputationalADT Fiat.ADTRefinement.GeneralBuildADTRefinements Coq.Bool.Bool Coq.ZArith.ZArith