~/jendhub

def AP.rep_add

bend-osdev-array@0.1.0.1 · PROOF.bend:1177

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base

1177def AP.rep_add(-T: Data, a: Nat, -b: Nat, -v: T) -> {List.replicate(T, Nat.add(a, b), v) == List.append(&2, T, List.replicate(T, a, v), List.replicate(T, b, v)) : List<&2, T>}:
1178  match a:
1179    case 0n:
1180      {==}
1181    case 1n+p:
1182      AP.con_cong(T, v, List.replicate(T, Nat.add(p, b), v), List.append(&2, T, List.replicate(T, p, v), List.replicate(T, b, v)), AP.rep_add(T, p, b, v))

Uses (6)

Used by (1)