proposition: Lemma parse_of_contract_minimal_parse_of_item_lt {len0} {str : String} {valid valid' : nonterminals_listT} {Hlt : length str < len0} {it} (p : minimal_parse_of_item (G := G) len0 valid str it) : parse_of_item__of__minimal_parse_of_item (contract_minimal_parse_of_item_lt (valid' := valid') Hlt p) = parse_of_item__of__minimal_parse_of_item p.
proof: Proof. destruct_head @MinimalParse.minimal_parse_of_item; simpl; try reflexivity. destruct_head @MinimalParse.minimal_parse_of_nonterminal; try reflexivity. unfold False_rect. match goal with | [ |- context[match ?e with end] ] => destruct e end. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.WellFoundedParse Fiat.Parsers.CorrectnessBaseTypes Fiat.Parsers.BaseTypes Fiat.Parsers.StringLike.Properties Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.MinimalParse Fiat.Parsers.WellFoundedParseProperties Fiat.Common