proposition: Lemma extension_in : forall (e : Ensf) (f : Elt -> Elt) (x : Elt), dans x e -> extension e f x = f x :>Elt.
proof: Proof. unfold extension in |- *. intros e f x dans_x_e. elim (extension_spec e f x). intro. tauto. Qed.
imports: Ensf Words more_words need