def AP.app_cong_l

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

import Base

998def AP.app_cong_l(-T: Data, -x: List<&2, T>, -y: List<&2, T>, -ys: List<&2, T>, e: {x == y : List<&2, T>}) -> {List.append(&2, T, x, ys) == List.append(&2, T, y, ys) : List<&2, T>}:
999  %e : {List.append(&2, T, x, ys) == List.append(&2, T, _, ys) : List<&2, T>}
1000  {==}