proposition: Lemma is_valid_nonterminal_of_to_nonterminal valids nt : sub_nonterminals_listT valids initial_nonterminals_data -> is_valid_nonterminal valids (of_nonterminal (to_nonterminal nt)) = is_valid_nonterminal valids nt.
proof: Proof. intro Hvalid. match goal with | [ |- ?lhs = ?rhs ] => destruct lhs eqn:?, rhs eqn:?; first [ reflexivity | exfalso ] end; repeat match goal with | [ H : is_valid_nonterminal _ _ = _ |- False ] => rewrite of_to_nonterminal in H | _ => congruence | _ => apply Hvalid; assumption | _ => rewrite initial_nonterminals_correct', <- initial_nonterminals_correct; apply Hvalid; assumption end. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.RelationClasses Coq.Setoids.Setoid Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes