proposition: Lemma Parse'_alternative_correct : Parse' = Parse'_alternative.
proof: Proof. Proof using. reflexivity. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat