proposition: Lemma pair_equal : forall (A B : Set) (x x' : A) (y y' : B), x = x' :>A -> y = y' :>B -> pair x y = pair x' y' :>A * B.
proof: Proof. intros A B x x' y y' X Y. rewrite X. rewrite Y. apply refl_equal. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_couple Ensf_inclus Ensf_map