+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).
+