fact: Fixpoint tq (f : Elt -> Prop) (e : Ensf) {struct e} : Ensf := match e return Ensf with | empty => empty | add x F => match Pdec f x return Ensf with | left fx => add x (tq f F) | right nfx => tq f F end end.
imports: Ensf