disco> 
Loading disco-live.disco...
Running tests...
  h: OK
Loaded.
disco> :test forall b1:Bool, b2:Bool. (g(b1) == g(b2)) -> (b1 == b2)
  - Certainly true: ∀b1, b2. g(b1) == g(b2) -> b1 == b2
    No counterexamples exist; all possible values were checked.
disco> :test forall x:N, y:N. (h(x) == h(y)) -> (x == y)
  - Possibly true: ∀x, y. h(x) == h(y) -> x == y
    Checked 100 possibilities without finding a counterexample.
disco> :test forall x:N, y:N. (l(x) == l(y)) -> (x == y)
  - Certainly false: ∀x, y. l(x) == l(y) -> x == y
    Found counterexample:
      x = 0
      y = 3
    - Certainly true: l(x) == l(y)
        - Left side:  F
        - Right side: F
    - Certainly false: x == y
        - Left side:  0
        - Right side: 3
disco> :test forall x:N, y:N. (j(x) == j(y)) -> (x == y)
  - Certainly false: ∀x, y. j(x) == j(y) -> x == y
    Found counterexample:
      x = 2
      y = 5
    - Certainly true: j(x) == j(y)
        - Left side:  17
        - Right side: 17
    - Certainly false: x == y
        - Left side:  2
        - Right side: 5
disco> :test forall x:N, y:N. (h(x) == h(y)) -> (x == y)
Loading disco-live.disco...
Running tests...
  h: OK
Loaded.
  - Possibly true: ∀x, y. h(x) == h(y) -> x == y
    Checked 100 possibilities without finding a counterexample.