match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝