(* BY-DEPTH DELAYED (BDD) TERM **********************************************)
inductive bdd: π«β¨pretermβ© β
-| bdd_oref: βn. bdd #n
-| bdd_iref: βt,n. bdd t β bdd πn.t
-| bdd_abst: βt. bdd t β bdd π.t
-| bdd_appl: βu,t. bdd u β bdd t β bdd @u.t
+| bdd_oref: βn. bdd (#n)
+| bdd_iref: βt,n. bdd t β bdd (πn.t)
+| bdd_abst: βt. bdd t β bdd (π.t)
+| bdd_appl: βu,t. bdd u β bdd t β bdd (@u.t)
| bdd_conv: βt1,t2. t1 β t2 β bdd t1 β bdd t2
.