(* BALANCE CONDITION FOR PATH ***********************************************)
-(* This condition applies to a structural path *)
+(* Note: this condition applies to a structural path *)
inductive pbc: predicate path ≝
| pbc_empty: pbc (𝐞)
| pbc_redex: ∀b. pbc b → pbc (𝗔◗b◖𝗟)