def internal_replicate_append_nil

bend-mathlib@0.8.1.0 · list.bend:1355

import Base

1355def internal_replicate_append_nil(-A: Data, n: Nat, -x: A) -> {List.append(&2, A, List.replicate(A, n, x), Nil{}) == List.replicate(A, n, x) : List<&2, A>}:
1356  match n:
1357    case 0n:
1358      {==}
1359    case 1n+p:
1360      %internal_replicate_append_nil(A, p, x) : {x <> List.append(&2, A, List.replicate(A, p, x), Nil{}) == x <> _ : List<&2, A>}
1361      {==}