List.internal_replicate_append_cons: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/list.bend as List
Lines 1363-1369 of bend-mathlib@0.8.1.0/list.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/list.bend&start_line=1363&end_line=1369

import Base

def 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>}:
  match n:
    case 0n:
      {==}
    case 1n+p:
      %internal_replicate_append_cons(A, p, x, acc) : {x <> List.append(&2, A, List.replicate(A, p, x), x <> acc) == x <> _ : List<&2, A>}
      {==}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.replicate
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat