| 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_appl: βu,t. bdd u β bdd t β bdd (οΌ u.t)
| bdd_conv: βt1,t2. t1 β t2 β bdd t1 β bdd t2
.