proposition: Lemma RLiteralTerm_beq_bl {t1 t2} (e1 : RLiteralTerm t1) (e2 : RLiteralTerm t2) : RLiteralTerm_beq e1 e2 = true -> { pf : t1 = t2 | eq_rect _ RLiteralTerm 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