def reverse_twice

qasim-bend-kit@0.1.0.2 · proof/JSON_StringProof.bend:57

import Base

57def reverse_twice(+text: String) -> {String.reverse(String.reverse(text)) == text : String}:
58    match text:
59        case SNil{}: {==}
60        case SCon{head, tail}:
61            Equal.trans(String, String.reverse(String.reverse(SCon{head, tail})),
62                String.reverse(String.reverse(tail) ++ SCon{head, SNil{}}), SCon{head, tail},
63                Equal.cong(String, String, String.reverse, String.reverse(SCon{head, tail}), String.reverse(tail) ++ SCon{head, SNil{}}, reverse_cons(head, tail)),
64                Equal.trans(String, String.reverse(String.reverse(tail) ++ SCon{head, SNil{}}),
65                    String.reverse(SCon{head, SNil{}}) ++ String.reverse(String.reverse(tail)), SCon{head, tail},
66                    reverse_append(String.reverse(tail), SCon{head, SNil{}}),
67                    Equal.cong(String, String, value => SCon{head, value}, String.reverse(String.reverse(tail)), tail, reverse_twice(tail))))