Definitions bool 1 Doc

At: comb for b2i wf

(b,z. b2i(b)) True
By: ProveOpCombTyping Thm* b:. b2i(b)
Generated subgoals:

None