law view_inj

lawful-arrays@0.1.0.0 · LAWS.bend:159

import Base
import lawful-arrays@0.1.0.0/defs.bend as D

159# Two perfect trees of the same depth with the same leaves are the same array.
160law view_inj:
161  for -T: Data
162  for a: Array<T>
163  for b: Array<T>
164  for d: Nat
165  for ha: {D.full(T, a, d) == True{} : Bool}
166  for hb: {D.full(T, b, d) == True{} : Bool}
167  for h: {D.view(T, a) == D.view(T, b) : List<&2, T>}
168  {a == b : Array<T>}