+ntheorem axiom_cond: ∀A:Ax.∀a:A.∀i:𝐈 a.a ◃ 𝐂 a i.
+#A; #a; #i; @2 i; #x; #H; @; napply H;
+nqed.
+
+nlemma hint_auto1 : ∀A,U,V. (∀x.x ∈ U → x ◃ V) → cover_set cover A U V.
+nnormalize; nauto.
+nqed.
+
+alias symbol "covers" (instance 1) = "covers".
+alias symbol "covers" (instance 2) = "covers set".
+alias symbol "covers" (instance 3) = "covers".
+ntheorem transitivity: ∀A:Ax.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
+#A; #a; #U; #V; #aU; #UV;
+nelim aU;
+##[ #c; #H; nauto;
+##| #c; #i; #HCU; #H; @2 i; nauto;
+##]
+nqed.
+
+ndefinition emptyset: ∀A.Ω^A ≝ λA.{x | False}.
+
+notation "∅" non associative with precedence 90 for @{ 'empty }.
+interpretation "empty" 'empty = (emptyset ?).
+
+naxiom EM : ∀A:Ax.∀a:A.∀i_star.(a ∈ 𝐂 a i_star) ∨ ¬( a ∈ 𝐂 a i_star).
+
+ntheorem th2_3 :
+ ∀A:Ax.∀a:A. a ◃ ∅ → ∃i. ¬ a ∈ 𝐂 a i.
+#A; #a; #H; nelim H;
+##[ #n; *;
+##| #b; #i_star; #IH1; #IH2;
+ ncases (EM … b i_star);
+ ##[##2: (* nauto; *) #W; @i_star; napply W;
+ ##| nauto;
+ ##]
+##]
+nqed.
+
+ninductive eq1 (A : Type[0]) : Type[0] → CProp[0] ≝
+| refl1 : eq1 A A.
+
+notation "hvbox( a break ∼ b)" non associative with precedence 40
+for @{ 'eqT $a $b }.
+
+interpretation "eq between types" 'eqT a b = (eq1 a b).
+