def internal_replicate_append_cons
bend-mathlib@0.8.1.0 · list.bend:1363
import bend-mathlib@0.8.1.0/list.bend as List
import Base
1363def internal_replicate_append_cons(-A: Data, n: Nat, -x: A, -acc: List<&2, A>) -> {List.append(&2, A, List.replicate(A, n, x), x <> acc) == x <> List.append(&2, A, List.replicate(A, n, x), acc) : List<&2, A>}:
1364 match n:
1365 case 0n:
1366 {==}
1367 case 1n+p:
1368 %internal_replicate_append_cons(A, p, x, acc) : {x <> List.append(&2, A, List.replicate(A, p, x), x <> acc) == x <> _ : List<&2, A>}
1369 {==}