fact: Definition transition_pont (x : Elt) : Elt := match x return Elt with | natural n => zero | couple e e' => couple (couple e zero) (couple epsilon (couple e' un)) | up e => zero | word w => zero end.
imports: Ensf Max Words Dec Reg Rat