def app2

bendtorch@1.3.0.0 · PROOF.bend:279

import Base

279# a ++ b == a2 ++ b2 from a == a2 and b == b2
280def app2(-A: Type, -a: List<&1, A>, -a2: List<&1, A>, -b: List<&1, A>, -b2: List<&1, A>, ea: {a == a2 : List<&1, A>}, eb: {b == b2 : List<&1, A>}) -> {List.append(&1, A, a, b) == List.append(&1, A, a2, b2) : List<&1, A>}:
281  Equal.trans(List<&1, A>, List.append(&1, A, a, b), List.append(&1, A, a2, b), List.append(&1, A, a2, b2), Equal.cong(List<&1, A>, List<&1, A>, z => List.append(&1, A, z, b), a, a2, ea), Equal.cong(List<&1, A>, List<&1, A>, z => List.append(&1, A, a2, z), b, b2, eb))