List.internal_replicate_append_nil: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/list.bend as List
Lines 1355-1361 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=1355&end_line=1361

import Base

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