JSONStringProof.reverse_twice: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend as JSONStringProof
Lines 57-67 of qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&start_line=57&end_line=67

import Base

def reverse_twice(+text: String) -> {String.reverse(String.reverse(text)) == text : String}:
    match text:
        case SNil{}: {==}
        case SCon{head, tail}:
            Equal.trans(String, String.reverse(String.reverse(SCon{head, tail})),
                String.reverse(String.reverse(tail) ++ SCon{head, SNil{}}), SCon{head, tail},
                Equal.cong(String, String, String.reverse, String.reverse(SCon{head, tail}), String.reverse(tail) ++ SCon{head, SNil{}}, reverse_cons(head, tail)),
                Equal.trans(String, String.reverse(String.reverse(tail) ++ SCon{head, SNil{}}),
                    String.reverse(SCon{head, SNil{}}) ++ String.reverse(String.reverse(tail)), SCon{head, tail},
                    reverse_append(String.reverse(tail), SCon{head, SNil{}}),
                    Equal.cong(String, String, value => SCon{head, value}, String.reverse(String.reverse(tail)), tail, reverse_twice(tail))))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.reverse
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=reverse_append
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=reverse_cons