-ntheorem th2_3 :
- âA:nAx.
- (âa:A.âi_star.(ây:đ a i_star.đ a i_star y = a) ⨠(ây:đ a i_star.đ a i_star y = a)) â
- âa:A. a â â
â âi:đ a. ÂŹ a \in Z
-#A; #EM; #a; #H; nelim H;
-##[ #n; *;
-##| #b; #i_star; #IH1; #IH2;
- ncases (EM b i_star);
- ##[##2: #W; @i_star; napply W;
- ##| *; #y_star; #E; nlapply (IH2 y_star); nrewrite > E; #OK; napply OK;
- ##]
-##]
-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).
-
-nrecord uAx : Type[1] â {
- uax_ : Ax;
- with_ : âa:uax_.đ a âź unit
-}.
-
-ndefinition uax : uAx â Ax.
-*; #A; #E; @ A (Îťx.unit); #a; ncases (E a);
-##[ #i; napply (đ a i);
-##| #i; nnormalize; #j; napply (đ a i j);
-##]
-nqed.
-
-ncoercion uax : âu:unAx. nAx â uax on _u : unAx to nAx.
-
-
-nlemma cor_2_5 : âA:unAx.âa:A.âi.a ⢠â
â ÂŹ(a â đđŚ[đ a i]).
-#A; #a; #i; #H; nelim H in i;
-##[ #w; *;
-##| #a; #i; #IH1; #IH2;
-
-
-
-
\ No newline at end of file
+ntheorem th_ch3: ÂŹâa:caxs.âx.Ď a x = h x.
+*; #a; #H;
+ncut (a â { x | x â â
}); ##[
+ napply (replace_char ⌠{ x | h x = O }); ##[ ##1,2: #x; ncases (Ph x); /2/; ##]
+ napply (replace_char ⌠{ x | Ď a x = O }); ##[##1,2: #x; nrewrite > (H x); //; ##]
+ napply (axiom_cond ⌠a one); ##] #H1;
+ncut (a â â
); ##[ napply (transitivity ⌠H1); //; ##] #H2;
+nlapply (col2_4 âŚH2); #H3;
+ncut (a â đ a one); ##[
+ nnormalize; ncases (Ph a); nrewrite > (H a); /2/; ##] #H4;
+/2/;
+nqed.
\ No newline at end of file