proposition: Lemma RLiteralNonConstructor_beq_bl {t1 t2} (e1 : RLiteralNonConstructor t1) (e2 : RLiteralNonConstructor t2) : RLiteralNonConstructor_beq e1 e2 = true -> { pf : t1 = t2 | eq_rect _ RLiteralNonConstructor e1 _ pf = e2 }.
proof: Proof. destruct e1, e2; t. Defined.
imports: Coq.Strings.Ascii Fiat.Parsers.Reflective.Syntax Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Equality Fiat.Common.BoolFacts