Nat.t = nat
     : Set
Nat.t = nat
     : Set
2 goals
  
  ============================
  True

goal 2 is:
 True
2 goals, goal 1 (?Goal)
  
  ============================
  True

goal 2 (?Goal0) is:
 True
1 goal
  
  ============================
  True
1 goal (?Goal0)
  
  ============================
  True
1 goal (?Goal0)
  
  ============================
  True

*** Unfocused goals:

goal 2 (?Goal1) is:
 True
goal 3 (?Goal) is:
 True
1 goal
  
  ============================
  True

*** Unfocused goals:

goal 2 is:
 True
goal 3 is:
 True
This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet -.

2 goals

goal 1 is:
 True
goal 2 is:
 True
This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet -.

2 goals

goal 1 (?Goal0) is:
 True
goal 2 (?Goal) is:
 True
This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet -.

1 goal

goal 1 is:
 True
This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet -.

1 goal

goal 1 (?Goal) is:
 True