law le_total_true

bend-mathlib@0.8.1.0 · order.bend:55

import Base

55# Totality as a Bool disjunction.
56law le_total_true:
57  for ~A: Data
58  for ~le: A -> A -> Bool
59  for ~le_total: @x: A -> @y: A -> {Bool.or(le(x, y), le(y, x)) == True{} : Bool}
60  for +a: A
61  for +b: A
62  {Bool.or(le(a, b), le(b, a)) == True{} : Bool}