V_______________________________________________________________ *)
include "basics/logic.ma".
+include "basics/core_notation/singl_1.ma".
+include "basics/core_notation/subseteq_2.ma".
(**** a subset of A is just an object of type A→Prop ****)
(* extensional equality *)
definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
+(* ≐ is typed as \doteq *)
notation "A ≐ B" non associative with precedence 45 for @{'eqP $A $B}.
interpretation "extensional equality" 'eqP a b = (eqP ? a b).
(* substraction *)
lemma substract_def:∀U.∀A,B:U→Prop. A-B ≐ A ∩ ¬B.
#U #A #B #w normalize /2/
-qed.
\ No newline at end of file
+qed.