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