def reverse_append

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

import Base

34def reverse_append(+left: String,
35                   +right: String) -> {String.reverse(left ++ right) == String.reverse(right) ++ String.reverse(left) : String}:
36    match left:
37        case SNil{}:
38            Equal.sym(String, String.reverse(right) ++ SNil{}, String.reverse(right), append_nil(String.reverse(right)))
39        case SCon{head, tail}:
40            Equal.trans(String, String.reverse(SCon{head, tail} ++ right),
41                String.reverse(tail ++ right) ++ SCon{head, SNil{}},
42                String.reverse(right) ++ String.reverse(SCon{head, tail}),
43                reverse_cons(head, tail ++ right),
44                Equal.trans(String, String.reverse(tail ++ right) ++ SCon{head, SNil{}},
45                    (String.reverse(right) ++ String.reverse(tail)) ++ SCon{head, SNil{}},
46                    String.reverse(right) ++ String.reverse(SCon{head, tail}),
47                    Equal.cong(String, String, value => value ++ SCon{head, SNil{}}, String.reverse(tail ++ right),
48                        String.reverse(right) ++ String.reverse(tail), reverse_append(tail, right)),
49                    Equal.trans(String, (String.reverse(right) ++ String.reverse(tail)) ++ SCon{head, SNil{}},
50                    String.reverse(right) ++ (String.reverse(tail) ++ SCon{head, SNil{}}),
51                    String.reverse(right) ++ String.reverse(SCon{head, tail}),
52                    append_assoc(String.reverse(right), String.reverse(tail), SCon{head, SNil{}}),
53                    Equal.cong(String, String, value => String.reverse(right) ++ value,
54                        String.reverse(tail) ++ SCon{head, SNil{}}, String.reverse(SCon{head, tail}),
55                        Equal.sym(String, String.reverse(SCon{head, tail}), String.reverse(tail) ++ SCon{head, SNil{}}, reverse_cons(head, tail))))))