+ntheorem col2_4 :
+ âA:uAx.âa:A. a â â
â ÂŹ a â đ a ?. ##[ (* bug *) ##2: nnormalize; napply one; ##]
+#A; #a; #H; nelim H;
+##[ #n; *;
+##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 ⌠H3); #H4; nauto;
+##]
+nqed.
+
+ndefinition Z : Ί^axs â { x | x â â
}.
+
+ntheorem cover_monotone: âA:Ax.âa:A.âU,V.U â V â a â U â a â V.
+#A; #a; #U; #V; #HUV; #H; nelim H;
+##[ nauto;
+##| #b; #i; #HCU; #W; @2 i; #x; nauto; ##]
+nqed.
+
+ntheorem th3_1: ÂŹâa:axs.Z â S a ⧠S a â Z.
+*; #a; *; #ZSa; #SaZ;
+ncut (a â Z); ##[
+ nlapply (axiom_cond ⌠a one); #AxCon; nchange in AxCon with (a â S a);
+ (* nauto; *) napply (cover_monotone ⌠AxCon); nassumption; ##] #H;
+ncut (a â â
); ##[ napply (transitivity ⌠H); #x; #E; napply E; ##] #H1;
+ncut (ÂŹ a â S a); ##[ napply (col2_4 ⌠H1); ##] #H2;
+ncut (a â S a); ##[ napply ZSa; napply H1; ##] #H3;
+nauto;
+nqed.
+
+include "nat/nat.ma".
+
+naxiom phi : nat â nat â nat.
+
+notation > "Ď" non associative with precedence 90 for @{ 'phi }.
+interpretation "phi" 'phi = phi.
+
+notation < "Ď a i" non associative with precedence 90 for @{ 'phi2 $a $i}.
+interpretation "phi2" 'phi2 a i = (phi a i).
+notation < "Ď a" non associative with precedence 90 for @{ 'phi1 $a }.
+interpretation "phi2" 'phi1 a = (phi a).
+
+ndefinition caxs : uAx.
+@; ##[ @ nat (Îť_.unit); #a; #_; napply { x | Ď a x = O } ##| #_; @; ##]
+nqed.
+
+
+alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
+unification hint 0 â ;
+ x â caxs
+ (* -------------- *) â˘
+ S x ⥠nat.
+
+naxiom h : nat â nat.
+
+alias symbol "eq" = "leibnitz's equality".
+alias symbol "eq" = "setoid1 eq".