+ [ apply (f a)
+ | apply (f1 a)]]
+qed.
+
+definition function_space_setoid1: setoid1 → setoid1 → setoid1.
+ intros (A B);
+ constructor 1;
+ [ apply (function_space1 A B);
+ | intros;
+ apply (∀a:A. proofs1 (eq1 ? (f a) (f1 a)));
+ |*: cases daemon] (* simplify;
+ intros;
+ apply (f1_ok ? ? x);
+ unfold proofs; simplify;
+ apply (refl1 A)
+ | simplify;
+ intros;
+ unfold proofs; simplify;
+ apply (sym1 B);
+ apply (f a)
+ | simplify;
+ intros;
+ unfold carr; unfold proofs; simplify;
+ apply (trans1 B ? (y a));
+ [ apply (f a)
+ | apply (f1 a)]] *)