proposition: Lemma pb_check_level_le {ch b} {n n'} (Hle : n <= n') : pb_check_level b ch n -> pb_check_level b ch n'.
proof: Proof. unfold pb_check_level. do 2 edestruct Compare_dec.gt_dec; trivial; try omega; simpl. destruct b; edestruct is_bin_op; trivial; edestruct is_close; edestruct is_open; unfold is_true; trivial. 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.BaseTypes Fiat.Common.List.Operations Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.Enumerable Fiat.Common.LogicFacts Fiat.Common.Equality