law view_inj_t

lawful-arrays@0.1.0.0 · proof_tree.bend:430

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

430law view_inj_t:
431  for -T: Data
432  for +d: Nat
433  for +ta: Tree<T>
434  for +tb: Tree<T>
435  for +ha: {D.full(T, fromT(T, ta), d) == True{} : Bool}
436  for +hb: {D.full(T, fromT(T, tb), d) == True{} : Bool}
437  for +he: {D.view(T, fromT(T, ta)) == D.view(T, fromT(T, tb)) : List<&2, T>}
438  {fromT(T, ta) == fromT(T, tb) : Array<T>}