]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / path_balanced.ma
index 017cfc5bae27c0dc38febdb6495b1f16eaf0bf33..c279d223107bcba197f550c6db84685f7d3395b2 100644 (file)
@@ -17,7 +17,7 @@ include "delayed_updating/notation/functions/class_b_0.ma".
 
 (* 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◖𝗟)