def node_equal
bendtorch-core@0.1.0.0 · src/storage/clone.bend:12
import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
import Base
12def node_equal(-T: Data, -a: Array<T>, -b: Array<T>, -x: Array<T>, -y: Array<T>,
13 left: {a == x : Array<T>}, right: {b == y : Array<T>}) ->
14 {ANode{a, b} == ANode{x, y} : Array<T>}:
15 Equal.trans(Array<T>, ANode{a, b}, ANode{x, b}, ANode{x, y},
16 Equal.cong(Array<T>, Array<T>, v => ANode{v, b}, a, x, left),
17 Equal.cong(Array<T>, Array<T>, v => ANode{x, v}, b, y, right))