hol.mm1

-- An axiomatization of (HOL light styled) HOL. The intent is to use hol.mm0 as the core theory
-- and this file as the proof of the core lemmas, and https://github.com/digama0/hz-to-mm0 will
-- translate proofs using these theorems when performing HOL kernel steps.
-- The public theorems in this file correspond roughly to the theorems in the Common HOL platform.

delimiter $ ( @ [ ! ? ~ $ $ . : ; ) ] $;
strict provable sort wff;

term im: wff > wff > wff; infixr im: $|-$ prec 0;
term an: wff > wff > wff; infixl an: $;$ prec 1;

axiom id (P: wff): $ P |- P $;
-- axiom mp (P Q: wff): $ P |- Q $ > $ P $ > $ Q $;
axiom syl (P Q R: wff): $ P |- Q $ > $ Q |- R $ > $ P |- R $;
axiom ian (G P Q: wff): $ G |- P $ > $ G |- Q $ > $ G |- P; Q $;
axiom anl (P Q: wff): $ P; Q |- P $;
axiom anr (P Q: wff): $ P; Q |- Q $;
theorem anld (h: $ G |- P; Q $): $ G |- P $ = '(syl h anl);
theorem anrd (h: $ G |- P; Q $): $ G |- Q $ = '(syl h anr);
theorem anwl (h: $ G |- Q $): $ G; P |- Q $ = '(syl anl h);
theorem anwr (h: $ P |- Q $): $ G; P |- Q $ = '(syl anr h);
theorem anwll (h: $ A |- P $): $ A; B; C |- P $ = '(anwl @ anwl h);
theorem anll: $ A; B; C |- A $ = '(anwl anl);
theorem anlr: $ A; B; C |- B $ = '(anwl anr);
theorem anllr: $ A; B; C; D |- B $ = '(anwl anlr);
theorem an3lr: $ A; B; C; D; E |- B $ = '(anwl anllr);
theorem anrl: $ A; (B; C) |- B $ = '(anwr anl);
theorem anrr: $ A; (B; C) |- C $ = '(anwr anr);
theorem anrlr: $ A; (B; C; D) |- C $ = '(anwr anlr);
theorem anrllr: $ A; (B; C; D; E) |- C $ = '(anwr anllr);
theorem mp (h1: $ G; A |- B $) (h2: $ G |- A $): $ G |- B $ = '(syl (ian id h2) h1);
theorem anasss (h: $ A; B; C |- D $): $ A; (B; C) |- D $ = '(syl (ian (ian anl anrl) anrr) h);
theorem anassrs (h: $ A; (B; C) |- D $): $ A; B; C |- D $ = '(syl (ian anll @ ian anlr anr) h);
theorem an32s (h: $ A; C; B |- D $): $ A; B; C |- D $ = '(syl (ian (ian anll anr) anlr) h);

strict sort type;

term bool: type;
term fun: type > type > type; infixr fun: $->$ prec 25;

sort term;
term ty: term > type > wff; infixl ty: $:$ prec 2;

term app: term > term > term; infixl app: $@$ prec 1000;
term lam {x: term}: type > term x > term;
notation lam {x: term} (t: type) (e: term x): term =
  ($\$:20) x ($:$:2) t ($.$:0) e;

axiom appT (G: wff) (A B: type) (f x: term):
  $ G |- f: A -> B $ > $ G |- x: A $ > $ G |- f @ x: B $;

axiom lamT (G: wff) (A B: type) {x: term} (t: term x):
  $ G; x: A |- t: B $ > $ G |- \ x: A. t: A -> B $;

-- These are not a complete set of inversion principles, but they are
-- enough for the core theory. We need existential type variables for the general case
axiom appTR1 (G: wff) (A B: type) (f x: term):
  $ G |- f @ x: B $ > $ G |- x: A $ > $ G |- f: A -> B $;
axiom appTR2 (G: wff) (A B: type) (f x: term):
  $ G |- f @ x: B $ > $ G |- f: A -> B $ > $ G |- x: A $;
axiom appTR22 (G: wff) (A B C: type) (f x y: term):
  $ G |- f @ x @ y: C $ > $ G |- f: A -> B -> C $ > $ G |- x: A; y: B $;

term eq: type > term;
axiom eqT (G: wff) (A: type): $ G |- eq A: A -> A -> bool $;
def eqc (A: type) (e1 e2: term): term = $ eq A @ e1 @ e2 $;
notation eqc (A: type) (e1 e2: term): term =
  ($=[$:50) A ($]$:0) e1 ($=$:50) e2;

theorem eqcT (h1: $ G |- e1: A $) (h2: $ G |- e2: A $): $ G |- =[A] e1 = e2: bool $ =
'(appT (appT eqT h1) h2);

term thm: term > wff; coercion thm: term > wff;

axiom thmR (G: wff) (A: term): $ G |- A $ > $ G |- A: bool $;

theorem eqR0 (h: $ G |- eq A @ a: A -> bool $): $ G |- a: A $ = '(appTR2 h eqT);

theorem eqR1 (h: $ G |- =[A] a = b $): $ G |- a: A $ = '(anld @ appTR22 (thmR h) eqT);
theorem eqR2 (h: $ G |- =[A] a = b $): $ G |- b: A $ = '(anrd @ appTR22 (thmR h) eqT);

axiom refl (G: wff) (A: type) (t: term):
  $ G |- t: A $ > $ G |- =[A] t = t $;

axiom aeq (G: wff) (A B: type) (f g a b: term):
  $ G |- =[A -> B] f = g $ > $ G |- =[A] a = b $ >
  $ G |- =[B] f @ a = g @ b $;

theorem aeq1 (h1: $ G |- =[A -> B] f = g $) (h2: $ G |- a: A $):
  $ G |- =[B] f @ a = g @ a $ = '(aeq h1 (refl h2));
theorem aeq2 (h1: $ G |- f: A -> B $) (h2: $ G |- =[A] a = b $):
  $ G |- =[B] f @ a = f @ b $ = '(aeq (refl h1) h2);

theorem bineq (h1: $ G |- f: A -> B -> C $)
  (h2: $ G |- =[A] a1 = a2 $) (h3: $ G |- =[B] b1 = b2 $):
  $ G |- =[C] f @ a1 @ b1 = f @ a2 @ b2 $ = '(aeq (aeq2 h1 h2) h3);
theorem bineq1 (h1: $ G |- f: A -> B -> C $)
  (h2: $ G |- =[A] a1 = a2 $) (h3: $ G |- b: B $):
  $ G |- =[C] f @ a1 @ b = f @ a2 @ b $ = '(bineq h1 h2 (refl h3));
theorem bineq2 (h1: $ G |- f: A -> B -> C $)
  (h2: $ G |- a: A $) (h3: $ G |- =[B] b1 = b2 $):
  $ G |- =[C] f @ a @ b1 = f @ a @ b2 $ = '(bineq h1 (refl h2) h3);

axiom leq (G: wff) (A B: type) {x: term} (a b: term x):
  $ G; x: A |- =[B] a = b $ >
  $ G |- =[A -> B] (\ x: A. a) = (\ x: A. b) $;

axiom beta (A B: type) {x: term} (G: wff x) (e: term x):
  $ G |- (\ x: A. e) @ x: B $ > $ G |- =[B] (\ x: A. e) @ x = e $;

pub theorem lamTR (G: wff x) (t: term x) (h1: $ G |- \ x: A. t: A -> B $):
  $ G; x: A |- t: B $ = '(eqR2 @ beta @ appT (anwl h1) anr);

def bi (a b) = $ =[bool] a = b $;
infixl bi: $<=>$ prec 20;

axiom eqmp (G: wff) (A B: term):
  $ G |- A <=> B $ > $ G |- A $ > $ G |- B $;

pub theorem trans (G: wff) (A: type) (a b c: term)
  (h1: $ G |- =[A] a = b $) (h2: $ G |- =[A] b = c $): $ G |- =[A] a = c $ =
'(eqmp (bineq2 eqT (eqR1 h1) h2) h1);

axiom ded (G: wff) (A B: term):
  $ G; A |- B $ > $ G; B |- A $ > $ G |- A <=> B $;

axiom cbvv (G: wff) (A B: type) {x y: term} (t: term x y):
  $ G |- t: B $ > $ G |- =[A -> B] (\ x: A. t) = (\ y: A. t) $;

axiom inst (G: wff) (A: type) {x: term} (t a: term x):
  $ G |- a: bool $ > $ G |- t: A $ > $ G; =[A] x = t |- a $ > $ G |- a $;

theorem sym (h: $ G |- =[A] a = b $): $ G |- =[A] b = a $ =
'(eqmp (bineq1 eqT h (eqR1 h)) (refl (eqR1 h)));

theorem eqmpr (h1: $ G |- B <=> A $) (h2: $ G |- A $): $ G |- B $ = '(eqmp (sym h1) h2);

theorem betae (G: wff x) (e: term x) (h1: $ G |- x: A $)
  (H: $ G |- =[A -> B] f = (\ x: A. e) $): $ G |- =[B] f @ x = e $ =
'(trans (aeq1 H h1) (beta @ appT (eqR2 H) h1));

abstract def T: term = $ =[bool -> bool] (\ x: bool. x) = (\ x: bool. x) $;
pub theorem TT: $ G |- T: bool $ = '(eqcT (!! lamT x anr) (lamT anr));
pub theorem T_DEF: $ G |- T <=> =[bool -> bool] (\ x: bool. x) = (\ x: bool. x) $ = '(refl TT);
pub theorem TRUTH: $ G |- T $ = '(refl (!! lamT x anr));
pub theorem EQT_ELIM (h: $ G |- P <=> T $): $ G |- P $ = '(eqmpr h TRUTH);
pub theorem EQT_INTRO (h: $ G |- P $): $ G |- P <=> T $ = '(ded TRUTH (anwl h));
theorem a1i (h: $ T |- P $): $ G |- P $ = '(syl TRUTH h);
theorem trud (h: $ G; T |- P $): $ G |- P $ = '(mp h TRUTH);

term tydef: term > type;
term abs: term > term;
term rep: term > term;
axiom absT: $ T |- P: A -> bool $ > $ G |- P @ t $ > $ G |- abs P: A -> tydef P $;
axiom repT: $ T |- P: A -> bool $ > $ G |- P @ t $ > $ G |- rep P: tydef P -> A $;
axiom abs_rep: $ T |- P: A -> bool $ > $ G |- P @ t $ >
  $ G; a: tydef P |- =[tydef P] abs P @ (rep P @ a) = a $;
axiom rep_abs: $ T |- P: A -> bool $ > $ G |- P @ t $ >
  $ G; r: A |- P @ r <=> =[A] rep P @ (abs P @ r) = r $;

axiom eta (G: wff) (A B: type) {x: term} (e: term x):
  $ G |- e: A -> B $ > $ G |- =[A -> B] (\ x: A. e @ x) = e $;

term sel: type > term;
axiom selT: $ G |- sel A: (A -> bool) -> A $;
axiom ax_sel (h: $ G |- P: A -> bool $) (h2: $ G |- P @ x $):
  $ G |- P @ (sel A @ P) $;
theorem selcT (e: term x) (h: $ G; x: A |- e: bool $): $ G |- sel A @ (\ x: A. e): A $ =
'(appT selT @ lamT h);

theorem betac (G: wff) (A B: type) {x: term} (t a b: term x)
  (h1: $ G; x: A |- a: B $) (h2: $ G |- t: A $)
  (h3: $ G |- b: B $) (h4: $ G; =[A] x = t |- =[B] a = b $):
  $ G |- =[B] (\ x: A. a) @ t = b $ =
'(!! inst x (eqcT (appT (lamT h1) h2) h3) h2 @
  trans (aeq2 (anwl @ lamT h1) @ sym anr) @
  trans (beta @ appT (anwl @ lamT h1) (eqR1 anr)) h4);

theorem cbv (t u: term x y)
  (h1: $ G; x: A |- t: B $) (h2: $ G; y: A |- u: B $)
  (h: $ G; =[A] x = y |- =[B] t = u $):
  $ G |- =[A -> B] (\ x: A. t) = (\ y: A. u) $ =
'(trans (sym @ eta @ lamT h1) @ leq @ betac (lamTR @ anwl @ lamT h1) anr h2 @
  syl (ian (anwl anl) anr) h);

abstract def and: term = $ \ p: bool. \ q: bool. =[(bool -> bool -> bool) -> bool]
  (\ f: bool -> bool -> bool. f @ p @ q) =
  (\ f: bool -> bool -> bool. f @ T @ T) $;
pub theorem andT: $ G |- and: bool -> bool -> bool $ =
'(!! lamT p @ !! lamT q @ eqcT
  (!! lamT f @ appT (appT anr anllr) anlr)
  (!! lamT f @ appT (appT anr TT) TT));
pub theorem AND_DEF: $ G |- =[bool -> bool -> bool] and =
  (\ p: bool. \ q: bool. =[(bool -> bool -> bool) -> bool]
    (\ f: bool -> bool -> bool. f @ p @ q) =
    (\ f: bool -> bool -> bool. f @ T @ T)) $ = '(refl andT);

def andc (a b) = $ and @ a @ b $; infixl andc: $/\$ prec 35;
theorem andcT (h1: $ G |- a: bool $) (h2: $ G |- b: bool $): $ G |- a /\ b : bool $ =
'(appT (appT andT h1) h2);
theorem andc_def (h1: $ G |- p: bool $) (h2: $ G |- q: bool $):
  $ G |- p /\ q <=>
    =[(bool -> bool -> bool) -> bool]
      (\ f: bool -> bool -> bool. f @ p @ q) =
      (\ f: bool -> bool -> bool. f @ T @ T) $ =
(focus
  (have 'H1 '(!! lamT f @ appT (appT anr TT) TT))
  (have 'H2 '(eqcT (!! lamT f @ appT (appT anr @ anwll h1) anlr) (anwl H1)))
  '(trans (aeq1
    (!! betac x (lamTR andT) h1 (lamT H2) @ leq @
      bineq1 eqT (leq @ bineq1 anr anllr anlr) (anwll H1)) h2) @
    !! betac y H2 h2 (eqcT (!! lamT f @ appT (appT anr @ anwl h1) (anwl h2)) H1) @
    bineq1 eqT (leq @ bineq2 anr (anwll h1) anlr) (anwl H1)));

pub theorem CONJ (h1: $ G |- a $) (h2: $ G |- b $): $ G |- a /\ b $ =
'(eqmpr (andc_def (thmR h1) (thmR h2)) @ !! leq f @
  bineq anr (EQT_INTRO @ anwl h1) (EQT_INTRO @ anwl h2));

theorem CONJ_PAIR (h: $ G |- a /\ b $): $ G |- a; b $ =
(focus
  (have 'H '(appTR22 (thmR h) andT))
  (have 'H1 '(anld H)) (have 'H2 '(anrd H))
  (def (case f x y z a b c) '(EQT_ELIM @
    trans (sym @
      betac (appT (appT anr @ anwl H1) @ anwl H2) (lamT ,f) ,x @
      trans (aeq1 (trans (aeq1 anr @ anwl H1) @
        anwl @ betac ,f H1 (lamT ,z) ,a) @ anwl H2) @
      anwl @ betac ,z H2 ,x ,y) @
    trans (aeq1 (eqmp (andc_def H1 H2) h) (!! lamT x ,f)) @
      !! betac f (appT (appT anr TT) TT) (lamT ,f) TT @
      trans (aeq1 (trans (aeq1 anr TT) @
        anwl @ betac ,f TT (lamT ,c) ,a) TT) @
      anwl @ betac ,c TT TT ,b))
  '(ian
    ,(case '(!! lamT y anlr) 'H1 '(refl @ anwl H1) '(anwl H1) '(leq anlr) '(refl TT) 'TT)
    ,(case '(!! lamT y anr) 'H2 'anr 'anr '(refl @ lamT anr) 'anr 'anr)));

pub theorem CONJUNCT1 (h: $ G |- a /\ b $): $ G |- a $ = '(anld @ CONJ_PAIR h);
pub theorem CONJUNCT2 (h: $ G |- a /\ b $): $ G |- b $ = '(anrd @ CONJ_PAIR h);

abstract def imp: term = $ \ p: bool. \ q: bool. (p /\ q) <=> p $;
pub theorem impT: $ G |- imp: bool -> bool -> bool $ =
'(!! lamT p @ !! lamT q @ eqcT (andcT anlr anr) anlr);
pub theorem IMP_DEF: $ G |- =[bool -> bool -> bool] imp =
  (\ p: bool. \ q: bool. (p /\ q) <=> p) $ = '(refl impT);

def impc (a b) = $ imp @ a @ b $; infixr impc: $==>$ prec 30;
theorem impcT (h1: $ G |- a: bool $) (h2: $ G |- b: bool $): $ G |- (a ==> b): bool $ =
'(appT (appT impT h1) h2);
theorem impc_def (h1: $ G |- p: bool $) (h2: $ G |- q: bool $):
  $ G |- (p ==> q) <=> ((p /\ q) <=> p) $ =
'(trans (aeq1 (!! betac x (lamTR impT) h1 (lamT @ eqcT (andcT (anwl h1) anr) (anwl h1)) @ leq @
  bineq eqT (bineq1 andT anlr anr) anlr) h2) @
  !! betac y (eqcT (andcT (anwl h1) anr) (anwl h1)) h2 (eqcT (andcT h1 h2) h1) @
  bineq1 eqT (bineq2 andT (anwl h1) anr) (anwl h1));

theorem impR (h: $ G |- p ==> q $): $ G |- p: bool; q: bool $ = '(appTR22 (thmR h) impT);

pub theorem MP (h1: $ G |- p ==> q $) (h2: $ G |- p $): $ G |- q $ =
'(CONJUNCT2 @ eqmpr (eqmp (impc_def (thmR h2) (anrd @ impR h1)) h1) h2);

pub theorem DISCH (hp: $ G |- p: bool $) (hq: $ G |- q: bool $) (h: $ G; p |- q $): $ G |- p ==> q $ =
'(eqmpr (impc_def hp hq) @ ded (CONJUNCT1 anr) (CONJ anr h));

pub theorem DISCH_ (hp: $ G |- p: bool $) (hq: $ G |- q: bool $) (h: $ G; (D; p) |- q $):
  $ G; D |- p ==> q $ =
'(DISCH (anwl hp) (anwl hq) @ anassrs h);

pub theorem UNDISCH (h: $ G |- p ==> q $): $ G; p |- q $ = '(MP (anwl h) anr);
pub theorem IMP_ANTISYM (h1: $ G |- p ==> q $) (h2: $ G |- q ==> p $): $ G |- p <=> q $ =
'(ded (UNDISCH h1) (UNDISCH h2));

pub theorem EQ_IMP1 (h: $ G |- p <=> q $): $ G |- p ==> q $ =
'(DISCH (eqR1 h) (eqR2 h) @ eqmp (anwl h) anr);
pub theorem EQ_IMP2 (h: $ G |- p <=> q $): $ G |- q ==> p $ = '(EQ_IMP1 @ sym h);

pub theorem IMP_ID (h: $ G |- p: bool $): $ G |- p ==> p $ = '(EQ_IMP1 @ refl h);
pub theorem IMP_TRANS (h1: $ G |- p ==> q $) (h2: $ G |- q ==> r $): $ G |- p ==> r $ =
'(DISCH (anld @ impR h1) (anrd @ impR h2) @ syl (ian anl (UNDISCH h1)) (UNDISCH h2));

abstract def all (A) = $ \ P: A -> bool. =[A -> bool] P = (\ x: A. T) $;
pub theorem allT: $ G |- all A: (A -> bool) -> bool $ =
'(!! lamT P @ eqcT anr @ !! lamT x TT);
pub theorem FORALL_DEF: $ G |- =[(A -> bool) -> bool] all A =
  (\ P: A -> bool. =[A -> bool] P = (\ x: A. T)) $ = '(refl allT);
theorem all_def (G: wff x) (P: term x) (h: $ G |- P: A -> bool $): $ G |- all A @ P <=>
  =[A -> bool] P = (\ x: A. T) $ =
'(!! betac p (lamTR allT) h (eqcT h @ a1i @ !! lamT x TT) (bineq1 eqT anr (a1i @ lamT TT)));

def allc {x: term} (A: type) (t: term x) = $ all A @ (\ x: A. t) $;
notation allc {x: term} (t: type) (e: term x): term = ($!$:20) x ($:$:2) t ($.$:0) e;
theorem allcT (t: term x) (h: $ G; x: A |- t: bool $): $ G |- !x: A. t: bool $ =
'(appT allT @ lamT h);
theorem alleq (t u: term x) (h: $ G; x: A |- t <=> u $): $ G |- (!x: A. t) <=> (!x: A. u) $ =
'(aeq2 allT @ leq h);

theorem specp (h: $ G |- t: A $) (h2: $ G |- all A @ P $): $ G |- P @ t $ =
'(EQT_ELIM @ trans (aeq1 (eqmp (all_def @ appTR2 (thmR h2) allT) h2) h) @
  !! betac x TT h TT (refl TT));

theorem spec (t a b: term x)
  (h0: $ G; x: A |- a: bool $) (h1: $ G |- t: A $) (h2: $ G |- b: bool $)
  (h3: $ G; =[A] x = t |- a <=> b $):
  $ G |- (!x: A. a) ==> b $ =
'(DISCH (allcT h0) h2 @ eqmp (anwl @ betac h0 h1 h2 h3) (specp (anwl h1) anr));

pub theorem SPEC (t a b: term x) (h1: $ G |- t: A $) (h2: $ G |- b: bool $)
  (h3: $ G; =[A] x = t |- a <=> b $) (h4: $ G |- !x: A. a $): $ G |- b $ =
'(MP (spec (lamTR @ appTR2 (thmR h4) allT) h1 h2 h3) h4);

pub theorem GEN (a: term x) (h: $ G; x: A |- a $): $ G |- !x: A. a $ =
'(eqmpr (all_def @ lamT @ thmR h) @ leq @ EQT_INTRO h);

pub theorem GEN_ (a: term x) (h: $ G; x: A; D |- a $): $ G; D |- !x: A. a $ =
'(GEN @ an32s h);

theorem betag1 (e: term x) (H: $ G |- =[A -> B] f = (\ x: A. e) $):
  $ G |- !x: A. =[B] f @ x = e $ =
'(GEN @ betae anr @ anwl H);

theorem betag2 (e: term x y) (H: $ G |- =[A -> B -> C] f = (\ x: A. \ y: B. e) $):
  $ G |- !x: A. !y: B. =[C] f @ x @ y = e $ =
'(GEN @ GEN @ betae anr @ anwl @ betae anr @ anwl H);

axiom AND_DEF1: $ G |- =[bool -> bool -> bool] and =
  (\ p: bool. \ q: bool. !t: bool. (p ==> q ==> t) ==> t) $; -- TODO

pub theorem IMP_ANTISYM_AX: $ G |- !t1: bool. !t2: bool.
  (t1 ==> t2) ==> (t2 ==> t1) ==> (t1 <=> t2) $ =
'(GEN @ GEN @ DISCH (impcT anlr anr) (impcT (impcT anr anlr) @ eqcT anlr anr) @
  DISCH_ (impcT anr anlr) (eqcT anlr anr) @ IMP_ANTISYM anrl anrr);

pub theorem ETA_AX (G: wff) (A B: type) {e x: term}:
  $ G |- !e: A -> B. =[A -> B] (\ x: A. e @ x) = e $ =
'(GEN @ eta anr);

abstract def ex (A) = $ \ P: A -> bool. !q: bool. (!x: A. P @ x ==> q) ==> q $;
theorem exT: $ G |- ex A: (A -> bool) -> bool $ =
'(!! lamT P @ !! allcT q @ impcT (!! allcT x @ impcT (appT anllr anr) anlr) anr);
pub theorem EXISTS_DEF: $ G |- =[(A -> bool) -> bool] ex A =
  (\ P: A -> bool. !q: bool. (!x: A. P @ x ==> q) ==> q) $ = '(refl exT);
theorem ex_def (G: wff x) (P: term) (h: $ G |- P: A -> bool $):
  $ G |- ex A @ P <=> (!q: bool. (!x: A. P @ x ==> q) ==> q) $ =
'(syl h @ !! betac p (lamTR exT) id
  (!! allcT q @ impcT (!! allcT x @ impcT (appT (anwl anl) anr) anlr) anr)
  (alleq @ bineq1 impT
    (alleq @ bineq1 impT (aeq1 anllr anr) anlr) anr));

abstract def exc {x: term} (A: type) (t: term x) = $ ex A @ (\ x: A. t) $;
notation exc {x: term} (t: type) (e: term x): term = ($?$:20) x ($:$:2) t ($.$:0) e;
theorem excT (t: term x) (h: $ G; x: A |- t: bool $): $ G |- ?x: A. t: bool $ =
'(appT exT @ lamT h);
theorem exeq (t u: term x) (h: $ G; x: A |- t <=> u $): $ G |- (?x: A. t) <=> (?x: A. u) $ =
'(aeq2 exT @ leq h);
theorem exc_def (p: term x) (h: $ G; x: A |- p: bool $):
  $ G |- (?x: A. p) <=> (!q: bool. (!x: A. p ==> q) ==> q) $ =
(begin (def h '(anwll @ lamT h)) (def h2 '(impcT (appT ,h anr) anlr))
  '(trans (ex_def @ lamT h) @ alleq @ bineq1 impT
    (trans (aeq2 allT @ !! cbv y x ,h2 ,h2 @ bineq1 impT (aeq2 ,h anr) anlr) @
      alleq @ bineq1 impT (beta @ appT ,h anr) anlr) anr));

pub theorem CHOOSE (p: term x) (hq: $ G |- q: bool $)
  (h1: $ G |- ?x: A. p $) (h2: $ G; x: A; p |- q $): $ G |- q $ =
(focus
  (have 'H '(appTR2 (thmR h1) exT))
  '(MP (SPEC hq
      (impcT (allcT @ impcT (lamTR H) (anwl hq)) hq)
      (bineq impT (alleq @ bineq2 impT (lamTR @ anwl H) anlr) anr)
      (eqmp (!! exc_def q2 _ @ lamTR H) h1)) @
    GEN @ DISCH (lamTR H) (anwl hq) h2));

theorem existsp (h1: $ G |- P: A -> bool $) (h2: $ G |- P @ x $): $ G |- ex A @ P $ =
(focus
  (have 'hx '(appTR2 (thmR h2) h1))
  (def H '(impcT (appT (anwll h1) anr) anlr))
  '(eqmpr (ex_def h1) @ !! GEN r @ DISCH (allcT ,H) anr @
    MP (UNDISCH @ !! spec y ,H (anwl hx) (impcT (anwl @ thmR h2) anr) @
      bineq1 impT (aeq2 (anwll h1) anr) anlr) @ anwll h2));

pub theorem EXISTS (t a b: term x)
  (h1: $ G; x: A |- a: bool $) (h2: $ G |- t: A $)
  (h3: $ G; =[A] x = t |- a <=> b $) (h4: $ G |- b $): $ G |- ?x: A. a $ =
'(existsp (lamT h1) @ eqmpr (betac h1 h2 (thmR h4) h3) h4);

theorem existsv (a: term x) (h1: $ G |- x: A $) (h2: $ G |- a $): $ G |- ?x: A. a $ =
(focus (have 'hl '(lamT @ anwl @ thmR h2)) '(existsp hl @ eqmpr (beta @ appT hl h1) h2));

theorem select_T {x: term} (G: wff x): $ G |- sel A @ (\ x: A. T): A $ =
'(a1i @ selcT TT);

theorem dummy {x: term} (h: $ G |- a: bool $) (h2: $ G; x: A |- a $): $ G |- a $ =
'(!! CHOOSE x h (EXISTS (anwl h) (!! select_T y)
    (EQT_INTRO @ syl (ian anl @ eqR1 anr) h2) TRUTH) (anwl h2));

theorem exsel (h1: $ G |- P: A -> bool $) (h: $ G |- ?x: A. P @ x $): $ G |- P @ (sel A @ P) $ =
'(CHOOSE (appT h1 @ appT selT h1) h @ ax_sel (anwll h1) anr);
theorem exsel2 (h1: $ G |- P: A -> bool $) (h: $ G |- ex A @ P $): $ G |- P @ (sel A @ P) $ =
'(exsel h1 @ eqmpr (aeq2 exT @ !! eta x h1) h);

theorem absT2 (h1: $ T |- P: A -> bool $) (h2: $ G |- ?x: A. P @ x $):
  $ G |- abs P: A -> tydef P $ = '(absT h1 @ exsel (a1i h1) h2);
theorem repT2 (h1: $ T |- P: A -> bool $) (h2: $ G |- ?x: A. P @ x $):
  $ G |- rep P: tydef P -> A $ = '(repT h1 @ exsel (a1i h1) h2);
theorem abs_rep2 (h1: $ T |- P: A -> bool $) (h2: $ G |- ?x: A. P @ x $):
  $ G; a: tydef P |- =[tydef P] abs P @ (rep P @ a) = a $ = '(abs_rep h1 @ exsel (a1i h1) h2);
theorem rep_abs2 (h1: $ T |- P: A -> bool $) (h2: $ G |- ?x: A. P @ x $):
  $ G; r: A |- P @ r <=> =[A] rep P @ (abs P @ r) = r $ = '(rep_abs h1 @ exsel (a1i h1) h2);

theorem absT3 (h1: $ T |- P: A -> bool $) (h2: $ G |- ex A @ P $):
  $ G |- abs P: A -> tydef P $ = '(absT h1 @ exsel2 (a1i h1) h2);
theorem repT3 (h1: $ T |- P: A -> bool $) (h2: $ G |- ex A @ P $):
  $ G |- rep P: tydef P -> A $ = '(repT h1 @ exsel2 (a1i h1) h2);
theorem abs_rep3 (h1: $ T |- P: A -> bool $) (h2: $ G |- ex A @ P $):
  $ G; a: tydef P |- =[tydef P] abs P @ (rep P @ a) = a $ = '(abs_rep h1 @ exsel2 (a1i h1) h2);
theorem rep_abs3 (h1: $ T |- P: A -> bool $) (h2: $ G |- ex A @ P $):
  $ G; r: A |- P @ r <=> =[A] rep P @ (abs P @ r) = r $ = '(rep_abs h1 @ exsel2 (a1i h1) h2);

abstract def or: term = $ \ p: bool. \ q: bool. !r: bool. (p ==> r) ==> (q ==> r) ==> r $;
pub theorem orT: $ G |- or: bool -> bool -> bool $ =
'(!! lamT p @ !! lamT q @ !! allcT r @
  impcT (impcT anllr anr) @ impcT (impcT anlr anr) anr);
pub theorem OR_DEF: $ G |- =[bool -> bool -> bool] or =
  (\ p: bool. \ q: bool. !r: bool. (p ==> r) ==> (q ==> r) ==> r) $ = '(refl orT);

def orc (a b) = $ or @ a @ b $; infixl orc: $\/$ prec 30;
theorem orcT (h1: $ G |- a: bool $) (h2: $ G |- b: bool $): $ G |- (a \/ b): bool $ =
'(appT (appT orT h1) h2);
theorem orc_def (h1: $ G |- p: bool $) (h2: $ G |- q: bool $):
  $ G |- (p \/ q) <=> (!r: bool. (p ==> r) ==> (q ==> r) ==> r) $ =
(begin
  (def (f p q) '(allcT @ impcT (impcT ,p anr) @ impcT (impcT ,q anr) anr))
  '(trans (aeq1 (!! betac x (lamTR orT) h1 (lamT ,(f '(anwll h1) 'anlr)) @ leq @
      alleq @ bineq1 impT (bineq1 impT anllr anr) @
      impcT (impcT anlr anr) anr) h2) @
    !! betac y ,(f '(anwll h1) 'anlr) h2 ,(f '(anwl h1) '(anwl h2)) @
    alleq @ bineq2 impT (impcT (anwll h1) anr) @
      bineq1 impT (bineq1 impT anlr anr) anr));

theorem orR (h: $ G |- p \/ q $): $ G |- p: bool; q: bool $ = '(appTR22 (thmR h) orT);

pub theorem DISJ1 (h1: $ G |- p $) (h2: $ G |- q: bool $): $ G |- p \/ q $ =
'(eqmpr (orc_def (thmR h1) h2) @ !! GEN r @
  DISCH (impcT (anwl @ thmR h1) anr) (impcT (impcT (anwl h2) anr) anr) @
  DISCH (impcT (anwll h2) anlr) anlr @ anwl @ MP anr @ anwll h1);

pub theorem DISJ1_ (h1: $ G; D |- p $) (h2: $ G |- q: bool $): $ G; D |- p \/ q $ =
'(DISJ1 h1 (anwl h2));

pub theorem DISJ2 (h1: $ G |- p: bool $) (h2: $ G |- q $): $ G |- p \/ q $ =
'(eqmpr (orc_def h1 (thmR h2)) @ !! GEN r @
  DISCH (impcT (anwl h1) anr) (impcT (impcT (anwl @ thmR h2) anr) anr) @
  anwl @ DISCH (impcT (anwl @ thmR h2) anr) anr @ MP anr @ anwll h2);

pub theorem DISJ2_ (h1: $ G |- p: bool $) (h2: $ G; D |- q $): $ G; D |- p \/ q $ =
'(DISJ2 (anwl h1) h2);

pub theorem DISJ_CASES (h: $ G |- p \/ q $) (hr: $ G |- r: bool $)
  (h1: $ G; p |- r $) (h2: $ G; q |- r $): $ G |- r $ =
(focus (have 'hp '(anld @ orR h)) (have 'hq '(anrd @ orR h))
  '(MP (MP (SPEC hr _ _ @ eqmp (!! orc_def x hp hq) h) @ DISCH hp hr h1) @ DISCH hq hr h2)
  '(impcT (impcT hp hr) @ impcT (impcT hq hr) hr)
  '(bineq impT (bineq2 impT (anwl hp) anr) @
    bineq impT (bineq2 impT (anwl hq) anr) anr));

pub theorem DISJ_CASES_ (h: $ G; D |- p \/ q $) (hr: $ G |- r: bool $)
  (h1: $ G; (D; p) |- r $) (h2: $ G; (D; q) |- r $): $ G; D |- r $ =
'(DISJ_CASES h (anwl hr) (anassrs h1) (anassrs h2));

abstract def F: term = $ !p: bool. p $;
pub theorem FT: $ G |- F: bool $ = '(!! allcT p anr);
pub theorem F_DEF: $ G |- F <=> (!p: bool. p) $ = '(refl FT);
pub theorem CONTR (p: term) (h: $ G |- p: bool $) (h2: $ G |- F $): $ G |- p $ =
'(!! SPEC x h h anr @ eqmp F_DEF h2);
pub theorem CONTR_ (p: term) (h: $ G |- p: bool $) (h2: $ G; D |- F $): $ G; D |- p $ =
'(CONTR (anwl h) h2);

abstract def not: term = $ \ p: bool. p ==> F $;
pub theorem notT: $ G |- not: bool -> bool $ = '(!! lamT p @ impcT anr FT);
pub theorem NOT_DEF: $ G |- =[bool -> bool] not = (\ p: bool. p ==> F) $ = '(refl notT);

def notc (p) = $ not @ p $;
prefix notc: $~$ prec 100;
theorem notc_def (h: $ G |- p: bool $): $ G |- ~p <=> p ==> F $ =
'(!! betac x (impcT anr FT) h (impcT h FT) @ bineq1 impT anr FT);
theorem notcT (h: $ G |- p: bool $): $ G |- ~p: bool $ = '(appT notT h);
theorem notR (h: $ G |- ~p $): $ G |- p: bool $ = '(appTR2 (thmR h) notT);

pub theorem NOT_ELIM (h: $ G |- ~p $): $ G |- p ==> F $ = '(eqmp (notc_def @ notR h) h);
pub theorem NOT_INTRO (h: $ G |- p ==> F $): $ G |- ~p $ = '(eqmpr (notc_def @ anld @ impR h) h);
pub theorem EQF_INTRO (h: $ G |- ~p $): $ G |- p <=> F $ =
'(IMP_ANTISYM (NOT_ELIM h) @ DISCH FT (notR h) @ CONTR (anwl @ notR h) anr);
pub theorem EQF_ELIM (h: $ G |- p <=> F $): $ G |- ~p $ = '(NOT_INTRO @ EQ_IMP1 h);
pub theorem NOT_FALSE: $ G |- ~F $ = '(NOT_INTRO @ IMP_ID FT);

pub theorem NOT_TRUE: $ G |- ~T <=> F $ =
'(EQF_INTRO @ NOT_INTRO @ DISCH (notcT TT) FT @ MP (NOT_ELIM anr) TRUTH);

abstract def eu (A) = $ \ P: A -> bool. ex A @ P /\
  (!x: A. !y: A. P @ x /\ P @ y ==> =[A] x = y) $;
pub theorem euT: $ G |- eu A: (A -> bool) -> bool $ =
'(!! lamT P @ andcT (appT exT anr) @ !! allcT x @ !! allcT y @
  impcT (andcT (appT anllr anlr) @ appT anllr anr) @ eqcT anlr anr);
pub theorem EU_DEF: $ G |- =[(A -> bool) -> bool] eu A =
  (\ P: A -> bool. ex A @ P /\ (!x: A. !y: A. P @ x /\ P @ y ==> =[A] x = y)) $ = '(refl euT);
theorem eu_def (G: wff x) (P: term) (h: $ G |- P: A -> bool $):
  $ G |- eu A @ P <=> ex A @ P /\ (!x: A. !y: A. P @ x /\ P @ y ==> =[A] x = y) $ =
'(syl h @ !! betac p (lamTR euT) id
  (andcT (appT exT id) @ !! allcT x @ !! allcT y @
    impcT (andcT (appT (anwl anl) anlr) @ appT (anwl anl) anr) @ eqcT anlr anr)
  (bineq andT (aeq2 exT anr) @ alleq @ alleq @
   bineq1 impT (bineq andT (aeq1 anllr anlr) (aeq1 anllr anr)) @
   eqcT anlr anr));

axiom EU_DEF1: $ G |- =[(A -> bool) -> bool] eu A =
  (\ P: A -> bool. ?t: A. P @ t /\ (!x: A. P @ x ==> =[A] x = t)) $; -- TODO

pub theorem SELECT_AX: $ G |- !P: A -> bool. !x: A. P @ x ==> P @ (sel A @ P) $ =
'(GEN @ GEN @ DISCH (appT anlr anr) (appT anlr @ appT selT anlr) @ ax_sel anllr anr);

axiom EXISTS_THM: $ G |- =[(A -> bool) -> bool] ex A = P @ (sel A @ P) $; -- TODO

pub theorem em (h: $ G |- p: bool $): $ G |- p \/ ~p $ =
(focus
  (have 'h2 '(notcT h)) (have 'H '(orcT h h2))
  (def (F k y t e)
    (def a '(orcT ,(k 'anr) @ anwl h))
    (def (f x) '(betac ,a ,x (orcT ,(k x) h) @ bineq1 orT ,y @ anwl h))
    '(eqmp ,(f '(selcT ,a)) @ ax_sel (lamT ,a) @ eqmpr ,(f t) @ DISJ1 ,e h))
  '(DISJ_CASES ,(F (fn (x) x) 'anr 'TT 'TRUTH) H _ (DISJ1 anr @ anwl h2))
  '(DISJ_CASES (anwl ,(F (fn (x) '(notcT ,x)) '(aeq2 notT anr) 'FT 'NOT_FALSE))
    (anwl H) _ (DISJ1 anr @ anwll h2))
  '(DISJ2 (anwll h) @ NOT_INTRO @ DISCH (anwll h) FT @ MP (NOT_ELIM anlr) @ eqmp _ anllr)
  '(anwr @ aeq2 selT @ !! leq x @
    trans (EQT_INTRO @ DISJ2 anr anl) @ sym (EQT_INTRO @ DISJ2 (notcT anr) anl)));
pub theorem em_ (h: $ G |- p: bool $): $ G; D |- p \/ ~p $ = '(anwl @ em h);

pub theorem BOOL_CASES_AX: $ G |- !t: bool. (t <=> T) \/ (t <=> F) $ =
'(trud @ GEN_ @ DISJ_CASES_ (em_ anr) (orcT (eqcT anr TT) (eqcT anr FT))
  (DISJ1_ (EQT_INTRO anrr) (eqcT anr FT))
  (DISJ2_ (eqcT anr TT) @ EQF_INTRO anrr));

pub theorem CCONTR (h: $ G |- p: bool $) (h2: $ G; ~p |- F $): $ G |- p $ =
'(DISJ_CASES (em h) h anr @ CONTR (anwl h) h2);

def COND (A) = $ \ t: bool. \ t1: A. \ t2: A. sel A @ (\ x: A.
  ((t <=> T) ==> =[A] x = t1) /\ ((t <=> F) ==> =[A] x = t2)) $;
theorem condT: $ G |- COND A: bool -> A -> A -> A $ =
'(!! lamT t @ !! lamT t1 @ !! lamT t2 @ !! selcT x @ andcT
  (impcT (eqcT an3lr TT) (eqcT anr anllr)) (impcT (eqcT an3lr FT) (eqcT anr anlr)));
theorem COND_DEF: $ G |- =[bool -> A -> A -> A] COND A =
  (\ t: bool. \ t1: A. \ t2: A. sel A @ (\ x: A.
    ((t <=> T) ==> =[A] x = t1) /\ ((t <=> F) ==> =[A] x = t2))) $ = '(refl condT);

def mk_pair (A B) = $ \ x: A. \ y: B. \ a: A. \ b: B. (=[A] a = x /\ =[B] b = y) $;
theorem mk_pairT: $ G |- mk_pair A B: A -> B -> A -> B -> bool $ =
'(!! lamT x @ !! lamT y @ !! lamT a @ !! lamT b @ andcT (eqcT anlr an3lr) (eqcT anr anllr));
theorem mk_pair_DEF: $ G |- =[A -> B -> A -> B -> bool] mk_pair A B =
  (\ x: A. \ y: B. \ a: A. \ b: B. (=[A] a = x /\ =[B] b = y)) $ = '(refl mk_pairT);

theorem pair_rep (hf: $ G |- f: A -> B -> C $): $ G |- ?x: C. ?a: A. ?b: B. =[C] x = f @ a @ b $ =
(focus
  (def (p f x y) '(appT (appT ,f ,x) ,y))
  (def (t1 f x a) '(eqcT ,x ,(p f a 'anr)))
  (def (t2 f x a) '(excT ,(t1 f x a)))
  (def f2 '(anwll hf)) (def f3 '(anwl ,f2)) (def f4 '(anwll ,f2)) (def f5 '(anwll ,f3))
  (have 'hab '(excT ,(t2 f3 'anllr 'anlr))) (have 'hx '(excT hab))
  (def (p1 f) (p f 'anlr 'anr)) (def p2 (p f3 'anllr 'anlr)) (def p3 (p f4 'an3lr 'anllr))
  '(!! dummy c hx @ !! dummy d (anwl hx) @
    EXISTS (lamTR @ anwll @ lamT hab) ,(p1 f2) (exeq @ exeq @ bineq1 eqT anllr ,(p1 f5)) @
    EXISTS ,(t2 f4 p3 'anlr) anlr (exeq @ bineq2 eqT ,p3 @ bineq1 (anwll @ anwll hf) anlr anr) @
    EXISTS ,(t1 f3 p2 'anllr) anr (bineq2 eqT ,p2 @ bineq2 (anwl @ anwll hf) anllr anr) @
    refl ,(p1 f2)));

theorem PROD_THM: $ G |- ?x: A -> B -> bool.
  ?a: A. ?b: B. =[A -> B -> bool] x = mk_pair A B @ a @ b $ = '(pair_rep mk_pairT);
theorem PROD_THM_T: $ T |- \ x: A -> B -> bool.
  ?a: A. ?b: B. =[A -> B -> bool] x = mk_pair A B @ a @ b: (A -> B -> bool) -> bool $ =
'(appTR2 (thmR PROD_THM) exT);
abstract def prod (A B) = $ tydef (\ x: A -> B -> bool.
  ?a: A. ?b: B. =[A -> B -> bool] x = mk_pair A B @ a @ b) $;
infixr prod: $#$ prec 30;
abstract def ABS_prod (A B) = $ abs (\ x: A -> B -> bool.
  ?a: A. ?b: B. =[A -> B -> bool] x = mk_pair A B @ a @ b) $;
pub theorem ABS_prodT: $ G |- ABS_prod A B: (A -> B -> bool) -> A # B $ =
'(absT3 (!! PROD_THM_T x u v) PROD_THM);
abstract def REP_prod (A B) = $ rep (\ x: A -> B -> bool.
  ?a: A. ?b: B. =[A -> B -> bool] x = mk_pair A B @ a @ b) $;
pub theorem REP_prodT: $ G |- REP_prod A B: A # B -> A -> B -> bool $ =
'(repT3 (!! PROD_THM_T x u v) PROD_THM);
theorem prod_tybij1 (h: $ G |- a: A # B $): $ G |-
  =[A # B] ABS_prod A B @ (REP_prod A B @ a) = a $ =
'(mp (abs_rep3 (!! PROD_THM_T x u v) PROD_THM) h);
theorem prod_tybij2 (h: $ G |- r: A -> B -> bool $): $ G |-
  (\ v: A -> B -> bool. ?y: A. ?u: B. =[A -> B -> bool] v = mk_pair A B @ y @ u) @ r <=>
  =[A -> B -> bool] REP_prod A B @ (ABS_prod A B @ r) = r $ =
'(mp (rep_abs3 (!! PROD_THM_T y u v) PROD_THM) h);
pub theorem PROD_BIJ1: $ G |- !a: A # B.
  =[A # B] ABS_prod A B @ (REP_prod A B @ a) = a $ =
'(GEN @ prod_tybij1 anr);
pub theorem PROD_BIJ2: $ G |- !r: A -> B -> bool.
  (\ v: A -> B -> bool. ?y: A. ?u: B. =[A -> B -> bool] v = mk_pair A B @ y @ u) @ r <=>
  =[A -> B -> bool] REP_prod A B @ (ABS_prod A B @ r) = r $ =
'(GEN @ prod_tybij2 anr);

abstract def pr (A B) = $ \ x: A. \ y: B. ABS_prod A B @ (mk_pair A B @ x @ y) $;
pub theorem prT: $ G |- pr A B: A -> B -> A # B $ =
'(!! lamT x @ !! lamT y @ appT ABS_prodT @ appT (appT mk_pairT anlr) anr);
pub theorem PAIR_DEF: $ G |- =[A -> B -> A # B] pr A B =
  (\ x: A. \ y: B. ABS_prod A B @ (mk_pair A B @ x @ y)) $ = '(refl prT);

axiom PAIR_EQ: $ G |- !x: A. !y: B. !a: A. !b: B.
  =[A # B] pr A B @ x @ y = pr A B @ a @ b <=> =[A] x = a /\ =[B] y = b $; -- TODO

axiom PAIR_SURJ: $ G |- !p: A # B. ?x: A. ?y: B. =[A # B] p = pr A B @ x @ y $; -- TODO

abstract def fst (A B) = $ \ p: A # B. sel A @ (\ x: A. ?y: B. =[A # B] p = pr A B @ x @ y) $;
pub theorem fstT: $ G |- fst A B: A # B -> A $ =
'(!! lamT p @ !! selcT x @ !! excT y @ eqcT anllr @ appT (appT prT anlr) anr);
pub theorem FST_DEF: $ G |- =[A # B -> A] fst A B =
  (\ p: A # B. sel A @ (\ x: A. ?y: B. =[A # B] p = pr A B @ x @ y)) $ = '(refl fstT);
axiom fstpr (h1: $ G |- x: A $) (h2: $ G |- y: B $):
  $ G |- =[A] fst A B @ (pr A B @ x @ y) = x $; -- TODO
pub theorem FST: $ G |- !x: A. !y: B. =[A] fst A B @ (pr A B @ x @ y) = x $ =
'(GEN @ GEN @ fstpr anlr anr);

abstract def snd (A B) = $ \ p: A # B. sel B @ (\ y: B. ?x: A. =[A # B] p = pr A B @ x @ y) $;
pub theorem sndT: $ G |- snd A B: A # B -> B $ =
'(!! lamT p @ !! selcT y @ !! excT x @ eqcT anllr @ appT (appT prT anr) anlr);
pub theorem SND_DEF: $ G |- =[A # B -> B] snd A B =
  (\ p: A # B. sel B @ (\ y: B. ?x: A. =[A # B] p = pr A B @ x @ y)) $ = '(refl sndT);
axiom sndpr (h1: $ G |- x: A $) (h2: $ G |- y: B $):
  $ G |- =[A] fst A B @ (pr A B @ x @ y) = y $; -- TODO
pub theorem SND: $ G |- !x: A. !y: B. =[A] fst A B @ (pr A B @ x @ y) = y $ =
'(GEN @ GEN @ sndpr anlr anr);

abstract def one_one (A B) = $ \ f: A -> B. !x1: A. !x2: A.
  =[B] f @ x1 = f @ x2 ==> =[A] x1 = x2 $;
pub theorem one_one_T: $ G |- one_one A B: (A -> B) -> bool $ =
'(!! lamT f @ !! allcT x1 @ !! allcT x2 @
  impcT (eqcT (appT anllr anlr) (appT anllr anr)) (eqcT anlr anr));
pub theorem one_one_BD: $ G |- =[(A -> B) -> bool] one_one A B =
  (\ f: A -> B. !x1: A. !x2: A. =[B] f @ x1 = f @ x2 ==> =[A] x1 = x2) $ = '(refl one_one_T);
theorem one_one_def (h: $ G |- f: A -> B $): $ G |- one_one A B @ f <=>
  (!x1: A. !x2: A. =[B] f @ x1 = f @ x2 ==> =[A] x1 = x2) $ =
'(!! betac g (lamTR one_one_T) h
  (!! allcT x1 @ !! allcT x2 @
    impcT (eqcT (appT (anwll h) anlr) (appT (anwll h) anr)) (eqcT anlr anr)) @
  alleq @ alleq @ bineq1 impT (bineq eqT (aeq1 anllr anlr) (aeq1 anllr anr)) (eqcT anlr anr));
pub theorem one_one_DEF: $ G |- !f: A -> B. one_one A B @ f <=>
  (!x1: A. !x2: A. =[B] f @ x1 = f @ x2 ==> =[A] x1 = x2) $ = '(GEN @ one_one_def anr);
pub theorem ONE_ONE (h: $ G |- f: A -> B $):
  $ G |- one_one A B @ f <=> (!x1: A. !x2: A.
    =[B] f @ x1 = f @ x2 ==> =[A] x1 = x2) $ =
'(betac (!! lamTR g one_one_T) h (!! allcT x1 @ !! allcT x2 @
    impcT (eqcT (appT (anwll h) anlr) (appT (anwll h) anr)) (eqcT anlr anr)) @
  alleq @ alleq @ bineq1 impT
    (bineq eqT (aeq1 anllr anlr) (aeq1 anllr anr)) (eqcT anlr anr));

abstract def onto (A B) = $ \ f: A -> B. !y: B. ?x: A. =[B] y = f @ x $;
pub theorem onto_T: $ G |- onto A B: (A -> B) -> bool $ =
'(!! lamT f @ !! allcT y @ !! excT x @ eqcT anlr @ appT anllr anr);
pub theorem onto_BD: $ G |- =[(A -> B) -> bool] onto A B =
  (\ f: A -> B. !y: B. ?x: A. =[B] y = f @ x) $ = '(refl onto_T);
theorem onto_def (h: $ G |- f: A -> B $): $ G |- onto A B @ f <=>
  (!y: B. ?x: A. =[B] y = f @ x) $ =
'(!! betac g (lamTR onto_T) h
  (!! allcT y @ !! excT x @ eqcT anlr @ appT (anwll h) anr) @
  alleq @ exeq @ bineq2 eqT anlr (aeq1 anllr anr));
pub theorem onto_DEF: $ G |- !f: A -> B. onto A B @ f <=>
  (!y: B. ?x: A. =[B] y = f @ x) $ = '(GEN @ onto_def anr);
pub theorem ONTO (h: $ G |- f: A -> B $):
  $ G |- onto A B @ f <=> (!y: B. ?x: A. =[B] y = f @ x) $ =
'(betac (!! lamTR g onto_T) h (!! allcT y @ !! excT x @ eqcT anlr @ appT (anwll h) anr) @
  alleq @ exeq @ bineq2 eqT anlr (aeq1 anllr anr));

term ind: type;
axiom inf (G: wff) {f: term}:
  $ G |- ?f: ind -> ind. one_one ind ind @ f /\ ~(onto ind ind @ f) $;

abstract def IND_SUC =
  $ sel (ind -> ind) @ (\ f: ind -> ind. ?z: ind.
    (!x1: ind. !x2: ind. =[ind] f @ x1 = f @ x2 ==> =[ind] x1 = x2) /\
    (!x: ind. ~(=[ind] f @ x = z))) $;
pub theorem IND_SUC_T: $ G |- IND_SUC: ind -> ind $ =
'(!! selcT f @ !! excT z @ andcT
  (!! allcT x1 @ !! allcT x2 @
    impcT (eqcT (appT an3lr anlr) (appT an3lr anr)) (eqcT anlr anr))
  (!! allcT x @ notcT @ eqcT (appT anllr anr) anlr));
pub theorem IND_SUC_DEF: $ G |- =[ind -> ind] IND_SUC =
  sel (ind -> ind) @ (\ f: ind -> ind. ?z: ind.
    (!x1: ind. !x2: ind. =[ind] f @ x1 = f @ x2 ==> =[ind] x1 = x2) /\
    (!x: ind. ~(=[ind] f @ x = z))) $ = '(refl IND_SUC_T);

axiom IND_SUC_0: $ G |- !x: ind. ~(=[ind] f @ IND_0 = z) $; -- TODO

axiom IND_SUC_INJ: $ G |- !x1: ind. !x2: ind.
  =[ind] IND_SUC @ x1 = IND_SUC @ x2 <=> =[ind] x1 = x2 $; -- TODO

abstract def IND_0 = $ sel ind @ (\ z: ind.
  (!x1: ind. !x2: ind. =[ind] IND_SUC @ x1 = IND_SUC @ x2 ==> =[ind] x1 = x2) /\
  (!x: ind. ~(=[ind] IND_SUC @ x = z))) $; -- TODO
pub theorem IND_0_T: $ G |- IND_0: ind $ =
'(!! selcT z @ andcT
  (!! allcT x1 @ !! allcT x2 @
    impcT (eqcT (appT IND_SUC_T anlr) (appT IND_SUC_T anr)) (eqcT anlr anr))
  (!! allcT x @ notcT @ eqcT (appT IND_SUC_T anr) anlr));
pub theorem IND_0_DEF: $ G |- =[ind] IND_0 = sel ind @ (\ z: ind.
  (!x1: ind. !x2: ind. =[ind] IND_SUC @ x1 = IND_SUC @ x2 ==> =[ind] x1 = x2) /\
  (!x: ind. ~(=[ind] IND_SUC @ x = z))) $ = '(refl IND_0_T); -- TODO

abstract def NUM_REP = $ \ k: ind. !P: ind -> bool.
  (!j: ind. (=[ind] j = IND_0 \/ (?i: ind. =[ind] j = IND_SUC @ i /\ P @ i)) ==> P @ j)
  ==> P @ k $;
pub theorem NUM_REP_T: $ G |- NUM_REP: ind -> bool $ =
'(!! lamT k @ !! allcT P @ impcT
   (!! allcT j @ impcT
      (orcT (eqcT anr IND_0_T) @ !! excT i @
        andcT (eqcT anlr (appT IND_SUC_T anr)) (appT anllr anr))
      (appT anlr anr))
   (appT anr anlr));
pub theorem NUM_REP_DEF: $ G |- =[ind -> bool] NUM_REP =
  (\ k: ind. !P: ind -> bool.
    (!j: ind. (=[ind] j = IND_0 \/ (?i: ind. =[ind] j = IND_SUC @ i /\ P @ i)) ==> P @ j)
    ==> P @ k) $ = '(refl NUM_REP_T);

axiom NUM_THM: $ G |- ?x: ind. NUM_REP @ x $; -- TODO
abstract def num = $ tydef NUM_REP $;
abstract def mk_num = $ abs NUM_REP $;
pub theorem mk_numT: $ G |- mk_num: ind -> num $ = '(absT2 NUM_REP_T @ !! NUM_THM x);
abstract def dest_num = $ rep NUM_REP $;
pub theorem dest_numT: $ G |- dest_num: num -> ind $ = '(repT2 NUM_REP_T @ !! NUM_THM x);
theorem num_tybij1 (h: $ G |- a: num $): $ G |- =[num] mk_num @ (dest_num @ a) = a $ =
'(mp (abs_rep2 NUM_REP_T @ !! NUM_THM x) h);
theorem num_tybij2 (h: $ G |- r: ind $):
  $ G |- NUM_REP @ r <=>  =[ind] dest_num @ (mk_num @ r) = r $ =
'(mp (rep_abs2 NUM_REP_T @ !! NUM_THM x) h);
pub theorem NUM_BIJ1: $ G |- !a: num. =[num] mk_num @ (dest_num @ a) = a $ =
'(GEN @ num_tybij1 anr);
pub theorem NUM_BIJ2: $ G |- !r: ind. NUM_REP @ r <=> =[ind] dest_num @ (mk_num @ r) = r $ =
'(GEN @ num_tybij2 anr);

abstract def _0 = $ mk_num @ IND_0 $;
axiom _0T: $ G |- _0: num $; -- TODO
axiom _0_DEF: $ G |- =[num] _0 = mk_num @ IND_0 $; -- TODO

abstract def suc = $ \ n: num. mk_num @ (IND_SUC @ (dest_num @ n)) $;
pub theorem sucT: $ G |- suc: num -> num $ =
'(!! lamT n @ appT mk_numT @ appT IND_SUC_T @ appT dest_numT anr);
theorem succT (h: $ G |- n: num $): $ G |- suc @ n: num $ = '(appT sucT h);
pub theorem suc_BD: $ G |- =[num -> num] suc =
  (\ n: num. mk_num @ (IND_SUC @ (dest_num @ n))) $ = '(refl sucT);
pub theorem suc_DEF: $ G |- !n: num. =[num] suc @ n =
  mk_num @ (IND_SUC @ (dest_num @ n)) $ = '(betag1 suc_BD);

abstract def NUMERAL = $ \ n: num. n $;
pub theorem NUMERAL_T: $ G |- NUMERAL: num -> num $ = '(!! lamT n anr);
theorem numcT (h: $ G |- n: num $): $ G |- NUMERAL @ n: num $ = '(appT NUMERAL_T h);
pub theorem NUMERAL_BD: $ G |- =[num -> num] NUMERAL = (\ n: num. n) $ = '(refl NUMERAL_T);
pub theorem NUMERAL_DEF: $ G |- !n: num. =[num] NUMERAL @ n = n $ = '(betag1 NUMERAL_BD);

local def c0 = $ NUMERAL @ _0 $; prefix c0: $0$ prec max;
theorem c0T: $ G |- 0: num $ = '(numcT _0T);

axiom NOT_SUC: $ G |- !n: num. ~(=[num] suc @ n = 0) $; -- TODO

axiom SUC_INJ: $ G |- !m: num. !n: num. =[num] suc @ m = suc @ n <=> =[num] m = n $; -- TODO

axiom num_CASES: $ G |- !m: num. =[num] m = 0 \/ (?n: num. =[num] m = suc @ n) $; -- TODO
axiom num_INDUCTION: $ G |- !P: num -> bool.
  P @ 0 /\ (!n: num. P @ n ==> P @ (suc @ n)) ==> (!n: num. P @ n) $; -- TODO
axiom num_RECURSION: $ G |- !e: A. !f: A -> num -> A. ?fn: num -> A.
  =[A] fn @ 0 = e /\ (!n: num. =[A] fn @ (suc @ n) = f @ (fn @ n) @ n) $; -- TODO

abstract def bit0 = $ sel (num -> num) @ (\ fn: num -> num.
  =[num] fn @ 0 = 0 /\
  (!n: num. =[num] fn @ (suc @ n) = suc @ (suc @ (fn @ n)))) $;
pub theorem bit0T: $ G |- bit0: num -> num $ =
'(!! selcT f @ andcT (eqcT (appT anr c0T) c0T) @
  !! allcT n @ eqcT (appT anlr @ succT anr) (succT @ succT @ appT anlr anr));
theorem bit0cT (h: $ G |- n: num $): $ G |- bit0 @ n: num $ = '(appT bit0T h);
pub theorem bit0_DEF: $ G |- =[num -> num] bit0 = sel (num -> num) @ (\ fn: num -> num.
  =[num] fn @ 0 = 0 /\
  (!n: num. =[num] fn @ (suc @ n) = suc @ (suc @ (fn @ n)))) $ = '(refl bit0T);

abstract def bit1 = $ \ n: num. suc @ (bit0 @ n) $;
pub theorem bit1T: $ G |- bit1: num -> num $ = '(!! lamT n @ succT @ bit0cT anr);
theorem bit1cT (h: $ G |- n: num $): $ G |- bit1 @ n: num $ = '(appT bit1T h);
pub theorem bit1_BD: $ G |- =[num -> num] bit1 = (\ n: num. suc @ (bit0 @ n)) $ = '(refl bit1T);
pub theorem bit1_DEF: $ G |- !n: num. =[num] bit1 @ n = suc @ (bit0 @ n) $ = '(betag1 bit1_BD);

local def c1 = $ NUMERAL @ (bit1 @ _0) $; prefix c1: $1$ prec max;
theorem c1T: $ G |- 1: num $ = '(numcT @ bit1cT _0T);

abstract def pre = $ sel (num -> num) @ (\ f: num -> num.
  =[num] f @ 0 = 0 /\ (!n: num. =[num] f @ (suc @ n) = n)) $;
pub theorem preT: $ G |- pre: num -> num $ =
'(!! selcT f @ andcT (eqcT (appT anr c0T) c0T) @ !! allcT n @ eqcT (appT anlr @ succT anr) anr);
pub theorem pre_DEF: $ G |- =[num -> num] pre = sel (num -> num) @ (\ f: num -> num.
  =[num] f @ 0 = 0 /\ (!n: num. =[num] f @ (suc @ n) = n)) $ = '(refl preT);
axiom PRE: $ G |- =[num] pre @ 0 = 0 /\ (!n: num. =[num] pre @ (suc @ n) = n) $; -- TODO

abstract def add = $ sel (num -> num -> num) @ (\ f: num -> num -> num.
  (!n: num. =[num] f @ 0 @ n = n) /\
  (!m: num. !n: num. =[num] f @ (suc @ m) @ n = suc @ (f @ m @ n))) $;
local def addc (a b) = $ add @ a @ b $; infixl addc: $+$ prec 65;
pub theorem addT: $ G |- add: num -> num -> num $ =
'(!! selcT f @ andcT (!! allcT n @ eqcT (appT (appT anlr c0T) anr) anr) @
  !! allcT m @ !! allcT n @ eqcT (appT (appT anllr @ succT anlr) anr) @
  succT @ appT (appT anllr anlr) anr);
theorem addcT (h1: $ G |- a: num $) (h2: $ G |- b: num $):
  $ G |- a + b: num $ = '(appT (appT addT h1) h2);
pub theorem add_DEF: $ G |- =[num -> num -> num]
  add = sel (num -> num -> num) @ (\ f: num -> num -> num.
    (!n: num. =[num] f @ 0 @ n = n) /\
    (!m: num. !n: num. =[num] f @ (suc @ m) @ n = suc @ (f @ m @ n))) $ = '(refl addT);
axiom ADD: $ G |- (!n: num. =[num] 0 + n = n) /\
  (!m: num. !n: num. =[num] suc @ m + n = suc @ (m + n)) $; -- TODO

abstract def mul = $ sel (num -> num -> num) @ (\ f: num -> num -> num.
  (!n: num. =[num] f @ 0 @ n = 0) /\
  (!m: num. !n: num. =[num] f @ (suc @ m) @ n = f @ m @ n + n)) $;
local def mulc (a b) = $ mul @ a @ b $; infixl mulc: $*$ prec 70;
pub theorem mulT: $ G |- mul: num -> num -> num $ =
'(!! selcT f @ andcT (!! allcT n @ eqcT (appT (appT anlr c0T) anr) c0T) @
  !! allcT m @ !! allcT n @ eqcT (appT (appT anllr @ succT anlr) anr) @
  addcT (appT (appT anllr anlr) anr) anr);
theorem mulcT (h1: $ G |- a: num $) (h2: $ G |- b: num $):
  $ G |- a * b: num $ = '(appT (appT mulT h1) h2);
pub theorem mul_DEF: $ G |- =[num -> num -> num]
  mul = sel (num -> num -> num) @ (\ f: num -> num -> num.
    (!n: num. =[num] f @ 0 @ n = 0) /\
    (!m: num. !n: num. =[num] f @ (suc @ m) @ n = f @ m @ n + n)) $ = '(refl mulT);
axiom MUL: $ G |- (!n: num. =[num] 0 * n = 0) /\
  (!m: num. !n: num. =[num] suc @ m * n = m * n + n) $; -- TODO
axiom MUL1: $ G |- (!n: num. =[num] 0 * n = 0) /\
  (!m: num. !n: num. =[num] suc @ m * n = n + m * n) $; -- TODO

abstract def exp = $ sel (num -> num -> num) @ (\ f: num -> num -> num.
  (!m: num. =[num] f @ m @ 0 = 1) /\
  (!m: num. !n: num. =[num] f @ m @ (suc @ n) = m * f @ m @ n)) $;
pub theorem expT: $ G |- exp: num -> num -> num $ =
'(!! selcT f @ andcT (!! allcT m @ eqcT (appT (appT anlr anr) c0T) c1T) @
  !! allcT m @ !! allcT n @ eqcT (appT (appT anllr anlr) (succT anr)) @
  mulcT anlr @ appT (appT anllr anlr) anr);
theorem expcT (h1: $ G |- a: num $) (h2: $ G |- b: num $):
  $ G |- exp @ a @ b: num $ = '(appT (appT expT h1) h2);
pub theorem exp_DEF: $ G |- =[num -> num -> num]
  exp = sel (num -> num -> num) @ (\ f: num -> num -> num.
    (!m: num. =[num] f @ m @ 0 = 1) /\
    (!m: num. !n: num. =[num] f @ m @ (suc @ n) = m * f @ m @ n)) $ = '(refl expT);
axiom EXP: $ G |- (!m: num. =[num] exp @ m @ 0 = 1) /\
  (!m: num. !n: num. =[num] exp @ m @ (suc @ n) = m * exp @ m @ n) $; -- TODO

abstract def le = $ sel (num -> num -> bool) @ (\ f: num -> num -> bool.
  (!m: num. f @ m @ 0 <=> =[num] m = 0) /\
  (!m: num. !n: num. f @ m @ (suc @ n) <=> =[num] m = suc @ n \/ f @ m @ n)) $;
pub theorem leT: $ G |- le: num -> num -> bool $ =
'(!! selcT f @ andcT (!! allcT m @ eqcT (appT (appT anlr anr) c0T) (eqcT anr c0T)) @
  !! allcT m @ !! allcT n @ eqcT (appT (appT anllr anlr) (succT anr)) @
  orcT (eqcT anlr @ succT anr) @ appT (appT anllr anlr) anr);
local def lec (a b) = $ le @ a @ b $; infixl lec: $<=$ prec 50;
theorem lecT (h1: $ G |- a: num $) (h2: $ G |- b: num $):
  $ G |- a <= b: bool $ = '(appT (appT leT h1) h2);
pub theorem le_DEF: $ G |- =[num -> num -> bool] le =
  sel (num -> num -> bool) @ (\ f: num -> num -> bool.
    (!m: num. f @ m @ 0 <=> =[num] m = 0) /\
    (!m: num. !n: num. f @ m @ (suc @ n) <=> =[num] m = suc @ n \/ f @ m @ n)) $ = '(refl leT);
axiom LE: $ G |- (!m: num. m <= 0 <=> =[num] m = 0) /\
  (!m: num. !n: num. m <= suc @ n <=> =[num] m = suc @ n \/ m <= n) $; -- TODO

abstract def lt = $ sel (num -> num -> bool) @ (\ f: num -> num -> bool.
  (!m: num. f @ m @ 0 <=> F) /\
  (!m: num. !n: num. f @ m @ (suc @ n) <=> =[num] m = n \/ f @ m @ n)) $;
pub theorem ltT: $ G |- lt: num -> num -> bool $ =
'(!! selcT f @ andcT (!! allcT m @ eqcT (appT (appT anlr anr) c0T) FT) @
  !! allcT m @ !! allcT n @ eqcT (appT (appT anllr anlr) (succT anr)) @
  orcT (eqcT anlr anr) @ appT (appT anllr anlr) anr);
local def ltc (a b) = $ lt @ a @ b $; infixl ltc: $<$ prec 50;
theorem ltcT (h1: $ G |- a: num $) (h2: $ G |- b: num $):
  $ G |- a < b: bool $ = '(appT (appT ltT h1) h2);
pub theorem lt_DEF: $ G |- =[num -> num -> bool] lt =
  sel (num -> num -> bool) @ (\ f: num -> num -> bool.
    (!m: num. f @ m @ 0 <=> F) /\
    (!m: num. !n: num. f @ m @ (suc @ n) <=> =[num] m = n \/ f @ m @ n)) $ = '(refl ltT);
axiom LT: $ G |- (!m: num. m < 0 <=> F) /\
  (!m: num. !n: num. m < suc @ n <=> =[num] m = n \/ m < n) $; -- TODO

axiom LE1: $ G |- !m: num. !n: num. m <= n <=> m < n \/ =[num] m = n $; -- TODO

abstract def ge = $ \ m: num. \ n: num. n <= m $;
pub theorem geT: $ G |- ge: num -> num -> bool $ = '(!! lamT m @ !! lamT n @ lecT anr anlr);
pub theorem ge_BD: $ G |- =[num -> num -> bool] ge = (\ m: num. \ n: num. n <= m) $ = '(refl geT);
pub theorem ge_DEF: $ G |- !m: num. !n: num. ge @ m @ n <=> n <= m $ = '(betag2 ge_BD);

abstract def gt = $ \ m: num. \ n: num. n < m $;
pub theorem gtT: $ G |- gt: num -> num -> bool $ = '(!! lamT m @ !! lamT n @ ltcT anr anlr);
pub theorem gt_BD: $ G |- =[num -> num -> bool] gt = (\ m: num. \ n: num. n < m) $ = '(refl gtT);
pub theorem gt_DEF: $ G |- !m: num. !n: num. gt @ m @ n <=> n < m $ = '(betag2 gt_BD);

abstract def even = $ sel (num -> bool) @ (\ f: num -> bool.
  (f @ 0 <=> T) /\ (!n: num. f @ (suc @ n) <=> ~(f @ n))) $;
pub theorem evenT: $ G |- even: num -> bool $ =
'(!! selcT f @ andcT (eqcT (appT anr c0T) TT) @
  !! allcT n @ eqcT (appT anlr @ succT anr) (notcT @ appT anlr anr));
pub theorem even_DEF: $ G |- =[num -> bool] even = sel (num -> bool) @ (\ f: num -> bool.
  (f @ 0 <=> T) /\ (!n: num. f @ (suc @ n) <=> ~(f @ n))) $ = '(refl evenT);
axiom EVEN: $ G |- =[num] even @ 0 = 0 /\ (!n: num. =[num] even @ (suc @ n) = n) $; -- TODO

abstract def odd = $ sel (num -> bool) @ (\ f: num -> bool.
  (f @ 0 <=> F) /\ (!n: num. f @ (suc @ n) <=> ~(f @ n))) $;
pub theorem oddT: $ G |- odd: num -> bool $ =
'(!! selcT f @ andcT (eqcT (appT anr c0T) FT) @
  !! allcT n @ eqcT (appT anlr @ succT anr) (notcT @ appT anlr anr));
pub theorem odd_DEF: $ G |- =[num -> bool] odd = sel (num -> bool) @ (\ f: num -> bool.
  (f @ 0 <=> F) /\ (!n: num. f @ (suc @ n) <=> ~(f @ n))) $ = '(refl oddT);
axiom ODD: $ G |- =[num] odd @ 0 = 0 /\ (!n: num. =[num] odd @ (suc @ n) = n) $; -- TODO
axiom ODD1: $ G |- !n: num. odd @ n <=> ~(even @ n) $; -- TODO

abstract def sub = $ sel (num -> num -> num) @ (\ f: num -> num -> num.
  (!m: num. =[num] f @ m @ 0 = m) /\
  (!m: num. !n: num. =[num] f @ m @ (suc @ n) = pre @ (f @ m @ n))) $;
local def subc (a b) = $ sub @ a @ b $; infixl subc: $-$ prec 65;
pub theorem subT: $ G |- sub: num -> num -> num $ =
'(!! selcT f @ andcT (!! allcT m @ eqcT (appT (appT anlr anr) c0T) anr) @
  !! allcT m @ !! allcT n @ eqcT (appT (appT anllr anlr) @ succT anr) @
  appT preT @ appT (appT anllr anlr) anr);
theorem subcT (h1: $ G |- a: num $) (h2: $ G |- b: num $):
  $ G |- a - b: num $ = '(appT (appT subT h1) h2);
pub theorem sub_DEF: $ G |- =[num -> num -> num]
  sub = sel (num -> num -> num) @ (\ f: num -> num -> num.
    (!m: num. =[num] f @ m @ 0 = m) /\
    (!m: num. !n: num. =[num] f @ m @ (suc @ n) = pre @ (f @ m @ n))) $ = '(refl subT);
axiom SUB: $ G |- (!m: num. =[num] m - 0 = m) /\
  (!m: num. !n: num. =[num] m - suc @ n = pre @ (m - n)) $; -- TODO

abstract def TYPEDEF (A B) {.rep} = $ \ P: A -> bool. \ rep: B -> A.
  one_one B A @ rep /\ (!x: A. P @ x <=> (?y: B. =[A] x = rep @ y)) $;
pub theorem TYPEDEF_T: $ G |- TYPEDEF A B: (A -> bool) -> (B -> A) -> bool $ =
'(!! lamT P @ !! lamT r @ andcT (appT one_one_T anr) @ !! allcT x @
  eqcT (appT anllr anr) @ !! excT y @ eqcT anlr @ appT anllr anr);
pub theorem TYPEDEF_DEF {rep}: $ G |- =[(A -> bool) -> (B -> A) -> bool] TYPEDEF A B =
  (\ P: A -> bool. \ rep: B -> A.
    one_one B A @ rep /\ (!x: A. P @ x <=> (?y: B. =[A] x = rep @ y))) $ = '(refl TYPEDEF_T);