fact: Definition est_dans_d'_2 (d : Ensf) (e y : Elt) : Prop := match y return Prop with | natural n => False | couple a e' => dans (couple (first e) (couple a (first e'))) d | up e => False | word w => False end.
imports: Ensf Max Words Dec Reg Rat