The [A | B]
is a disjunction pattern. It is the same idea as case analysis in functional programming languages.
In this case you are creating two subgoals. One where t
is known to be a leaf with the natural number nleaf
as its argument, and another where t
is introduced as a Node
with the arguments nnode
, t1
, and t2
.
Either way another argument h : is_single_nBT ? = true
is introduced where ?
is either Leaf nleaf
or Node nnode t1 t2
.