Comment: core_2_intro
`Introduces a variety of general-purpose definitions and`
`theorems. `

Definition: ycomb
`Y ==  λf.((λx.(f (x x))) (λx.(f (x x))))`

Definition: recind-ycomb
`Y' ==  λf,x. letrec x(y) = f x y in x(x)`

Definition: pi2
`snd(t) ==  let x,y = t in y`

Definition: pi1
`fst(t) ==  let x,y = t in x`

Definition: so_apply1
`x[s] ==  x s`

Definition: so_apply2
`x[s1;s2] ==  x s1 s2`

Definition: so_apply3
`x[s1;s2;s3] ==  x s1 s2 s3`

Definition: so_apply4
`x[s1;s2;s3;s4] ==  x s1 s2 s3 s4`

Definition: so_apply5
`x[s1;s2;s3;s4;s5] ==  x s1 s2 s3 s4 s5`

Definition: so_apply6
`x[a;b;c;d;e;f] ==  x a b c d e f`

Definition: so_apply7
`x[a;b;c;d;e;f;g] ==  x a b c d e f g`

Definition: so_apply8
`x[a;b;c;d;e;f;g;h] ==  x a b c d e f g h`

Definition: so_apply9
`x[a;b;c;d;e;f;g;h;i] ==  x a b c d e f g h i`

Definition: so_apply10
`x[a;b;c;d;e;f;g;h;i;j] ==  x a b c d e f g h i j`

Definition: so_apply11
`x[a;b;c;d;e;f;g;h;i;j;k] ==  x a b c d e f g h i j k`

Definition: so_apply12
`x[a;b;c;d;e;f;g;h;i;j;k;l] ==  x a b c d e f g h i j k l`

Definition: so_apply13
`x[a;b;c;d;e;f;g;h;i;j;k;l;m] ==  x a b c d e f g h i j k l m`

Definition: so_apply14
`x[a;b;c;d;e;f;g;h;i;j;k;l;m;n] ==  x a b c d e f g h i j k l m n`

Definition: infix_ap
`x f y ==  f x y`

Definition: so_lambda1
`λ2x.t[x] ==  λx.t[x]`

Definition: so_lambda2
`λ2x y.t[x; y] ==  λx,y. t[x; y]`

Definition: so_lambda3
`so_lambda(x,y,z.t[x;`
`                  y;`
`                  z]) ==`
`  λx,y,z. t[x;`
`            y;`
`            z]`

Definition: so_lambda4
`so_lambda(x,y,z,w.t[x;`
`                    y;`
`                    z;`
`                    w]) ==`
`  λx,y,z,w. t[x;`
`              y;`
`              z;`
`              w]`

Definition: so_lambda5
`so_lambda(x,y,z,w,v.t[x;`
`                      y;`
`                      z;`
`                      w;`
`                      v]) ==`
`  λx,y,z,w,v. t[x;`
`                y;`
`                z;`
`                w;`
`                v]`

Definition: so_lambda6
`so_lambda(x,y,z,u,v,w.t[x;`
`                       y;`
`                       z;`
`                       u;`
`                       v;`
`                       w]) ==`
`  λx,y,z,u,v,w. t[x;`
`                 y;`
`                 z;`
`                 u;`
`                 v;`
`                 w]`

Definition: so_lambda7
`so_lambda(x,y,z,u,v,w,q.t[x;`
`                         y;`
`                         z;`
`                         u;`
`                         v;`
`                         w;`
`                         q]) ==`
`  λx,y,z,u,v,w,q. t[x;`
`                   y;`
`                   z;`
`                   u;`
`                   v;`
`                   w;`
`                   q]`

Definition: so_lambda8
`so_lambda(x,y,z,u,v,w,q,p.t[x;`
`                            y;`
`                            z;`
`                            u;`
`                            v;`
`                            w;`
`                            q;`
`                            p]) ==`
`  λx,y,z,u,v,w,q,p. t[x;`
`                      y;`
`                      z;`
`                      u;`
`                      v;`
`                      w;`
`                      q;`
`                      p]`

Definition: so_lambda9
`so_lambda(x,y,z,u,v,w,q,p,r.t[x;`
`                              y;`
`                              z;`
`                              u;`
`                              v;`
`                              w;`
`                              q;`
`                              p;`
`                              r]) ==`
`  λx,y,z,u,v,w,q,p,r. t[x;`
`                        y;`
`                        z;`
`                        u;`
`                        v;`
`                        w;`
`                        q;`
`                        p;`
`                        r]`

Definition: label
`...\$L... t ==  t`

Definition: guard
`{T} ==  T`

Definition: show
`The term show(x) unfolds to x. It has a special display form that makes it`
`easy to spot.  We make a conversion ShowAddrC addr that folds `show` at the`
`given addr. That helps when working with conversions so that we can`
`easily see what term is at a given address. ⋅`

⇒⇒` x `⇐⇐` ==  x`

Definition: error
`??? ==  "error"`

Definition: prop
`ℙ ==  Type`

Definition: cand
`A c∧ B ==  A × B`

Definition: parameter
`parm{i} ==  !null_abstraction`

Comment: top_com
`⌜Top⌝ is the type that contains all terms`

Definition: top
`⌜Top⌝ is the type that contains all terms⋅`

`Top ==  ⋂x:Void. Void`

Lemma: top_wf
`Top ∈ Type`

Lemma: istype-top
`istype(Top)`

Lemma: istype-void
`istype(Void)`

Lemma: istype-int
`istype(ℤ)`

Lemma: istype-atom
`istype(Atom)`

Definition: uall
`This is "uniform" universal quantification.`
`Evidence for ⌜∀[x:A]. B[x]⌝ must be something that is a member of ⌜B[x]⌝`
`whenever ⌜x ∈ A⌝. Such evidence is independent of the choice of ⌜x ∈ A⌝. ⋅`

`∀[x:A]. B[x] ==  ⋂x:A. B[x]`

Lemma: uall_wf
`∀[A:Type]. ∀[B:A ⟶ ℙ].  (∀[x:A]. B[x] ∈ ℙ)`

Lemma: isect_wf
`∀[A:Type]. ∀[B:A ⟶ ℙ].  (⋂x:A. B[x] ∈ ℙ)`

Lemma: base_wf
`Base ∈ Type`

Lemma: istype-base
`istype(Base)`

Lemma: image-type_wf
`∀[A:Type]. ∀[f:Base].  (Image(A,f) ∈ Type)`

Definition: tunion_def
`The union of a family types B[x], x ∈ A is obtained from the type `
`x:A × B[x] of all pairs <a, b>, a ∈ A, b ∈ B[a] by projection onto the`
`second component.  That means that b ∈ ⋃x:A.B[x]  if for some a ∈ A,`
`<a, b> ∈ x:A × B[x].⋅`

`⋃x:A.B[x] ==  Image((x:A × B[x]),(λp.(snd(p))))`

Lemma: tunion_wf
`∀[A:Type]. ∀[B:A ⟶ Type].  (⋃x:A.B[x] ∈ Type)`

Lemma: set_wf
`∀[A:Type]. ∀[B:A ⟶ Type].  ({a:A| B[a]}  ∈ Type)`

Lemma: set-elim
`∀[A:Type]. ∀[B:A ⟶ Type].  ∀x:Image((a:A × B[a]),(λp.(fst(p)))). ((x ∈ A) ∧ (↓B[x]))`

Lemma: equal-wf-base
`∀[A:Type]. ∀[a,b:Base].  (a = b ∈ A ∈ ℙ)`

Lemma: trivial-equal
`∀[A:Type]. ∀[a:A].  (a = a ∈ A)`

Definition: respects-equality
`respects-equality(S;T) ==  ∀x,y:Base.  ((x = y ∈ S) `` (x ∈ T) `` (x = y ∈ T))`

Lemma: respects-equality_wf
`∀[S,T:Type].  (respects-equality(S;T) ∈ Type)`

Lemma: base-respects-equality
`∀[T:Type]. respects-equality(Base;T)`

Lemma: respects-equality-trivial
`∀[T:Type]. respects-equality(T;T)`

Lemma: respects-equality-set-trivial
`∀[T:Type]. ∀[P:T ⟶ ℙ].  respects-equality(T;{x:T| P[x]} )`

Lemma: respects-equality-set-trivial2
`∀[T:Type]. ∀[P:T ⟶ ℙ].  respects-equality({x:T| P[x]} ;T)`

Lemma: respects-equality-set
`∀[A,T:Type]. ∀[P:T ⟶ ℙ].  (respects-equality(A;T) `` respects-equality(A;{x:T| P[x]} ))`

Lemma: respects-equality-sets
`∀[A,T:Type]. ∀[P:T ⟶ ℙ]. ∀[Q:A ⟶ ℙ].  (respects-equality(A;T) `` respects-equality({x:A| Q[x]} ;{x:T| P[x]} ))`

Lemma: equal-wf
`∀[X,Y,A:Type].  (respects-equality(Y;A) `` respects-equality(X;A) `` (∀[a:X]. ∀[b:Y].  (a = b ∈ A ∈ ℙ)))`

Lemma: equal_wf
`∀[A:Type]. ∀[a,b:A].  (a = b ∈ A ∈ ℙ)`

Lemma: equal-wf-T-base
`∀[T:Type]. ∀[a:T]. ∀[b:Base].  (a = b ∈ T ∈ ℙ)`

Lemma: equal-wf-base-T
`∀[T:Type]. ∀[a:Base]. ∀[b:T].  (a = b ∈ T ∈ ℙ)`

Lemma: change-equality-type
`∀[A,B:Type].  (respects-equality(A;B) `` (∀x,y:A.  ((x = y ∈ A) `` (x ∈ B) `` (x = y ∈ B))))`

Definition: subtype_rel
`A ⊆r B ==  λx.x ∈ A ⟶ B`

Lemma: subtype_rel_wf
`∀[A,B:Type].  (A ⊆r B ∈ Type)`

Definition: istype
`istype(T) ==  T ⊆r T`

Lemma: istype_wf
`∀[T:Type]. (istype(T) ∈ Type)`

Lemma: istype-universe
`∀[T:Type]. istype(T)`

Lemma: respects-equality_weakening
`∀[T,S:Type].  ((S = T ∈ Type) `` respects-equality(S;T))`

Lemma: respects-equality-function
`∀[A,A':Type]. ∀[B:A ⟶ Type]. ∀[B':A' ⟶ Type].`
`  ((A' ⊆r A) `` (∀a:A'. respects-equality(B[a];B'[a])) `` respects-equality(a:A ⟶ B[a];a:A' ⟶ B'[a]))`

Lemma: false_wf
`False ∈ ℙ`

Lemma: istype-false
`istype(False)`

Lemma: void_wf
`Void ∈ Type`

Lemma: int-wf
`ℤ ∈ Type`

Comment: no apply_wf
`The "true" _wf for apply would be`
`⌜∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:x:A ⟶ B[x]]. ∀[a:A].  (f a ∈ B[a])⌝`

`an "approximation" is `
`⌜∀[A,B:Type]. ∀[f:x:A ⟶ B]. ∀[a:A].  (f a ∈ B)⌝`

`Both of these are true, but if we add them to the library`
`then they would be used by type inference and by Auto`

`At present, they interfere too much with the working of other tactic.`
`So, until we understand the problems better, we do not add a _wf lemma`
`for apply.⋅`

Lemma: infix_ap_wf
`∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[x:A]. ∀[y:B].  (x f y ∈ C)`

Lemma: lambda-wf
`∀[A,B:Type]. ∀[f:A ⟶ B].  (λx.f[x] ∈ A ⟶ B)`

Lemma: product-wf
`∀[A:Type]. ∀[B:A ⟶ Type].  (a:A × B[a] ∈ Type)`

Lemma: exists_wf
`∀[A:Type]. ∀[B:A ⟶ ℙ].  (∃a:A. B[a] ∈ ℙ)`

Lemma: and_wf
`∀[A,B:ℙ].  (A ∧ B ∈ ℙ)`

Lemma: cand_wf
`∀[A,B:ℙ].  (A c∧ B ∈ ℙ)`

Lemma: or_wf
`∀[A,B:ℙ].  (A ∨ B ∈ ℙ)`

Lemma: function-wf
`∀[A:Type]. ∀[B:A ⟶ Type].  (a:A ⟶ B[a] ∈ Type)`

Lemma: all_wf
`∀[A:Type]. ∀[B:A ⟶ ℙ].  (∀a:A. B[a] ∈ ℙ)`

Lemma: sq_exists_wf
`∀[A:Type]. ∀[B:A ⟶ ℙ].  (∃a:A [B[a]] ∈ ℙ)`

Lemma: set-wf
`∀[A:Type]. ∀[P:A ⟶ ℙ].  ({a:A| P[a]}  ∈ Type)`

Lemma: union-wf
`∀[A,B:Type].  (A + B ∈ Type)`

`∀[x,y:ℤ].  (x + y ∈ ℤ)`

Lemma: minus_wf
`∀[x:ℤ]. (-x ∈ ℤ)`

Lemma: multiply_wf
`∀[x,y:ℤ].  (x * y ∈ ℤ)`

Lemma: subtract_wf
`∀[x,y:ℤ].  (x - y ∈ ℤ)`

Lemma: uall_subtype
`∀[F:Type ⟶ Type]. ∀[A:Type].  ((∀[A:Type]. F[A]) ⊆r F[A])`

Definition: uimplies
`This is "uniform" implication.`
`Evidence for (a `` b) is a function from evidence for a to evidence for b,`
`but evidence for (b supposing a) is something that is evidence for b`
`as long as a is not empty (i.e. supposing that a has evidence).`

`Thus, the evidence must be "uniform" because it does not depend on`
`the the evidence for a. ⋅`

`b supposing a ==  ⋂:a. b`

Lemma: uimplies-wf
`∀[A:ℙ]. ∀[B:⋂a:A. ℙ].  (B supposing A ∈ ℙ)`

Lemma: implies-wf
`∀[A:ℙ]. ∀[B:⋂a:A. ℙ].  (A `` B ∈ ℙ)`

Definition: rev_uimplies
`rev_uimplies(P;Q) ==  P supposing Q`

Lemma: rev_uimplies_wf
`∀[P,Q:ℙ].  (rev_uimplies(P;Q) ∈ ℙ)`

Definition: uiff
`uiff(P;Q) ==  Q supposing P ∧ P supposing Q`

Lemma: uiff_wf
`∀[P,Q:ℙ].  (uiff(P;Q) ∈ ℙ)`

Lemma: iff_weakening_uiff
`∀[P,Q:ℙ].  (uiff(P;Q) `` (P `⇐⇒` Q))`

Lemma: iff_weakening_equal
`∀[A,B:Type].  {A `⇐⇒` B} supposing A = B ∈ Type`

Lemma: implies_weakening_uimplies
`∀[P,Q:ℙ].  (Q supposing P `` {P `` Q})`

Lemma: rev_implies_weakening_rev_uimplies
`∀[P,Q:ℙ].  (rev_uimplies(P;Q) `` {P `` Q})`

Lemma: uiff_functionality_wrt_uiff
`∀[P1,P2,Q1,Q2:ℙ].  ({P1 `⇐⇒` P2} `` {Q1 `⇐⇒` Q2} `` {uiff(P1;Q1) `⇐⇒` uiff(P2;Q2)})`

Lemma: uiff_functionality_wrt_uiff2
`∀[P1,P2,Q1,Q2:ℙ].  ({P1 `⇐⇒` P2} `` {Q1 `⇐⇒` Q2} `` {uiff(P1;Q1) `⇐⇒` uiff(P2;Q2)})`

Lemma: uimplies_functionality_wrt_uimplies
`∀[P1,P2,Q1,Q2:ℙ].  ({P1 supposing P2} `` {Q2 supposing Q1} `` {Q1 supposing P1 `` Q2 supposing P2})`

Lemma: uimplies_functionality_wrt_uiff
`∀[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)} `` {uiff(Q1;Q2)} `` {uiff(Q1 supposing P1;Q2 supposing P2)})`

Lemma: uimplies-iff-squash-implies
`∀[P,Q:ℙ].  (Q supposing P `⇐⇒` (↓P) `` Q)`

Lemma: and_functionality_wrt_uimplies
`∀[P1,P2,Q1,Q2:ℙ].  ({P2 supposing P1} `` {Q2 supposing Q1} `` {P2 ∧ Q2 supposing P1 ∧ Q1})`

Lemma: and_functionality_wrt_rev_uimplies
`∀[P1,P2,Q1,Q2:ℙ].  ({rev_uimplies(P1;P2)} `` {rev_uimplies(Q1;Q2)} `` {rev_uimplies(P1 ∧ Q1;P2 ∧ Q2)})`

Lemma: and_functionality_wrt_uiff
`∀[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)} `` {uiff(Q1;Q2)} `` {uiff(P1 ∧ Q1;P2 ∧ Q2)})`

Lemma: not_functionality_wrt_uimplies
`∀[P,Q:ℙ].  ({P supposing Q} `` {¬Q supposing ¬P})`

Lemma: not_functionality_wrt_uiff
`∀[P,Q:ℙ].  ({uiff(P;Q)} `` {uiff(¬P;¬Q)})`

Lemma: uall_functionality_wrt_iff
`∀[S,T:Type]. ∀[P,Q:S ⟶ ℙ].  (∀[x:S]. (P[x] `⇐⇒` Q[x])) `` {∀[x:S]. P[x] `⇐⇒` ∀[y:T]. Q[y]} supposing S = T ∈ Type`

Lemma: uimplies_antisymmetry
`∀[P,Q:ℙ].  (Q supposing P `` P supposing Q `` uiff(P;Q))`

Lemma: uimplies_transitivity
`∀[P,Q,R:ℙ].  (Q supposing P `` R supposing Q `` {R supposing P})`

Lemma: uiff_transitivity
`∀[P,Q,R:ℙ].  (uiff(P;Q) `` uiff(Q;R) `` uiff(P;R))`

Lemma: uiff_transitivity2
`∀[P,Q,R:ℙ].  (uiff(P;Q) `` (Q = R ∈ ℙ) `` uiff(P;R))`

Lemma: uiff_transitivity3
`∀[P,Q,R:ℙ].  ((P = Q ∈ ℙ) `` uiff(Q;R) `` uiff(P;R))`

Comment: CORE_WF_THEOREMS
`Wf theorems for definitions introduced`
`in core_1 theory.  `

Lemma: true_wf
`True ∈ ℙ`

Lemma: istype-true
`istype(True)`

Lemma: squash_wf
`∀[A:ℙ]. (↓A ∈ ℙ)`

Lemma: squash-test
`∀[P:ℙ]. (P `` (↓P))`

Lemma: guard_wf
`∀[T:Type]. ({T} ∈ Type)`

Lemma: unit_wf
`Unit ∈ Type`

Lemma: not_wf
`∀[A:ℙ]. (¬A ∈ ℙ)`

Lemma: member-not
`∀[A:ℙ]. ∀[z:Top].  λx.z ∈ ¬A supposing ¬A`

Lemma: comb_for_not_wf
`λA,z. (¬A) ∈ A:ℙ ⟶ (↓True) ⟶ ℙ`

Lemma: rev_implies_wf
`∀[A,B:ℙ].  (A `` B ∈ ℙ)`

Lemma: comb_for_rev_implies_wf
`λA,B,z. (A `` B) ∈ A:ℙ ⟶ B:ℙ ⟶ (↓True) ⟶ ℙ`

Lemma: iff_wf
`∀[A,B:ℙ].  (A `⇐⇒` B ∈ ℙ)`

Lemma: comb_for_iff_wf
`λA,B,z. (A `⇐⇒` B) ∈ A:ℙ ⟶ B:ℙ ⟶ (↓True) ⟶ ℙ`

Lemma: nequal_wf
`∀[A:Type]. ∀[x,y:A].  (x ≠ y ∈ A  ∈ ℙ)`

Lemma: member_wf
`∀[A:Type]. ∀[a:A].  (a ∈ A ∈ Type)`

Comment: COMBS_acom
`Common Combinators`

Definition: icomb
`I ==  λx.x`

Lemma: icomb_wf
`∀[A:Type]. (I ∈ A ⟶ A)`

Definition: kcomb
`K ==  λx,y. x`

Lemma: kcomb_wf
`∀[A,B:Type].  (K ∈ A ⟶ B ⟶ A)`

Definition: scomb
`S ==  λx,y,z. (x z (y z))`

Lemma: scomb_wf
`∀[A,B,C:Type].  (S ∈ (A ⟶ B ⟶ C) ⟶ (A ⟶ B) ⟶ A ⟶ C)`

Comment: PRODUCT_DEFS_acom
`Projection functions for pairs`

Lemma: pi2_wf
`∀[A:Type]. ∀[B:A ⟶ Type]. ∀[p:a:A × B[a]].  (snd(p) ∈ B[fst(p)])`

Lemma: pi1_wf
`∀[A:Type]. ∀[B:A ⟶ Type]. ∀[p:a:A × B[a]].  (fst(p) ∈ A)`

Lemma: pair_eta_rw
`∀[A:Type]. ∀[B:A ⟶ Type]. ∀[p:a:A × B[a]].  (<fst(p), snd(p)> = p ∈ (a:A × B[a]))`

Lemma: respects-equality-product
`∀[A,A':Type]. ∀[B:A ⟶ Type]. ∀[B':A' ⟶ Type].`
`  (respects-equality(A;A')`
`  `` (∀a:Base. ((a ∈ A) `` (a ∈ A') `` respects-equality(B[a];B'[a])))`
`  `` respects-equality(a:A × B[a];a:A' × B'[a]))`

`let x,y,z = a in `
`t[x;`
`  y;`
`  z] ==`
`  let x,zz = a `
`  in let y,z = zz `
`     in t[x;`
`          y;`
`          z]`

`let w,x,y,z = a `
`in t[w;`
`     x;`
`     y;`
`     z]   ==`
`  let w,zz1 = a `
`  in let x,zz2 = zz1 `
`     in let y,z = zz2 `
`        in t[w;`
`             x;`
`             y;`
`             z]`

`let a,b,c,d,e = u in v[a;`
`                       b;`
`                       c;`
`                       d;`
`                       e] ==`
`  let a,zz1 = u `
`  in let b,zz2 = zz1 `
`     in let c,zz3 = zz2 `
`        in let d,e = zz3 `
`           in v[a;`
`                b;`
`                c;`
`                d;`
`                e]`

`let a,b,c,d,e,f = u in `
`v[a;`
` b;`
` c;`
` d;`
` e;`
` f] ==`
`  let a,zz1 = u `
`  in let b,zz2 = zz1 `
`     in let c,zz3 = zz2 `
`        in let d,zz4 = zz3 `
`           in let e,f = zz4 `
`              in v[a;`
`                  b;`
`                  c;`
`                  d;`
`                  e;`
`                  f]`

`let a,b,c,d,e,f,g = u in `
` v[a;`
`  b;`
`  c;`
`  d;`
`  e;`
`  f;`
`  g] ==`
`  let a,zz1 = u `
`  in let b,zz2 = zz1 `
`     in let c,zz3 = zz2 `
`        in let d,zz4 = zz3 `
`           in let e,zz5 = zz4 `
`              in let f,g = zz5 `
`                 in v[a;`
`                     b;`
`                     c;`
`                     d;`
`                     e;`
`                     f;`
`                     g]`

Lemma: all_functionality_wrt_uimplies
`∀[S,T:Type]. ∀[P:S ⟶ ℙ]. ∀[Q:T ⟶ ℙ].`
`  (∀x:T. {Q[x] supposing P[x]}) `` {∀x:T. Q[x] supposing ∀x:S. P[x]} supposing S = T ∈ Type`

Lemma: all_functionality_wrt_uiff
`∀[S,T:Type]. ∀[P:S ⟶ ℙ]. ∀[Q:T ⟶ ℙ].`
`  (∀x:T. {uiff(P[x];Q[x])}) `` {uiff(∀x:S. P[x];∀x:T. Q[x])} supposing S = T ∈ Type`

Comment: UNIT_DEFS_acom
`Inhabitant of Unit type`

Definition: it
`⋅ ==  Ax`

Definition: exposed-it
`exposed-it ==  Ax`

Lemma: it_wf
`⋅ ∈ Unit`

Lemma: unit_triviality
`∀[a:Unit]. (a = ⋅ ∈ Unit)`

Comment: CONSTR_PROPERTIES_com
`Predicates for constructive properties of propositions, and`
`lemmas characterizing how these predicates are inherited.`

`Worthwhile sometime redoing thms for soft abstractions`
`in terms of the underlying hard abstractions / primitives.`

Definition: decidable
`Dec(P) ==  P ∨ (¬P)`

Lemma: decidable_wf
`∀[A:ℙ]. (Dec(A) ∈ ℙ)`

Lemma: decidable__or
`∀[P,Q:ℙ].  (Dec(P) `` Dec(Q) `` Dec(P ∨ Q))`

Lemma: decidable__and
`∀[P,Q:ℙ].  (Dec(P) `` (P `` Dec(Q)) `` Dec(P ∧ Q))`

Lemma: decidable__and2
`∀[P:ℙ]. ∀[Q:⋂:P. ℙ].  (Dec(P) `` (P `` Dec(Q)) `` Dec(P ∧ Q))`

Lemma: decidable__implies
`∀[P:ℙ]. ∀[Q:⋂p:P. ℙ].  (Dec(P) `` (P `` Dec(Q)) `` Dec(P `` Q))`

Lemma: decidable__false
`Dec(False)`

Lemma: decidable__true
`Dec(True)`

Lemma: decidable__not
`∀[P:ℙ]. (Dec(P) `` Dec(¬P))`

Lemma: decidable__iff
`∀[P,Q:ℙ].  (Dec(P) `` Dec(Q) `` Dec(P `⇐⇒` Q))`

Lemma: atom_subtype_base
`Atom ⊆r Base`

Lemma: decidable__atom_equal
`∀a,b:Atom.  Dec(a = b ∈ Atom)`

Lemma: iff_preserves_decidability
`∀[A,B:ℙ].  (Dec(A) `` (A `⇐⇒` B) `` Dec(B))`

Definition: stable
`Stable{P} ==  P supposing ¬¬P`

Lemma: stable_wf
`∀[A:ℙ]. (Stable{A} ∈ ℙ)`

Lemma: stable__not
`∀[P:ℙ]. Stable{¬P}`

Lemma: stable__false
`Stable{False}`

Lemma: stable__and
`∀[P,Q:ℙ].  (Stable{P} `` Stable{Q} `` Stable{P ∧ Q})`

Lemma: stable__all
`∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∀x:T. Stable{P[x]}) `` Stable{∀x:T. P[x]})`

Lemma: stable__implies
`∀[P,Q:ℙ].  (Stable{P} `` Stable{Q `` P})`

Lemma: stable__function_equal
`∀[A,B:Type]. ∀[f,g:A ⟶ B].  Stable{f = g ∈ (A ⟶ B)} supposing ∀x:A. Stable{(f x) = (g x) ∈ B}`

Lemma: stable__from_decidable
`∀[P:ℙ]. (Dec(P) `` Stable{P})`

Definition: sq_stable
`SqStable(P) ==  (↓P) `` P`

Lemma: sq_stable_wf
`∀[A:ℙ]. (SqStable(A) ∈ ℙ)`

Lemma: sq_stable_functionality
`∀[A,B:ℙ].  ((A `⇐⇒` B) `` (SqStable(A) `⇐⇒` SqStable(B)))`

Lemma: sq_stable__and
`∀[P:ℙ]. ∀[Q:⋂p:P. ℙ].  (SqStable(P) `` (P `` SqStable(Q)) `` SqStable(P ∧ Q))`

Lemma: sq_stable__implies
`∀[P,Q:ℙ].  (SqStable(Q) `` SqStable(P `` Q))`

Lemma: sq_stable__uimplies
`∀[P,Q:ℙ].  (SqStable(Q) `` SqStable(Q supposing P))`

Lemma: sq_stable__iff
`∀[P,Q:ℙ].  (SqStable(P) `` SqStable(Q) `` SqStable(P `⇐⇒` Q))`

Lemma: sq_stable__uiff
`∀[P,Q:ℙ].  (SqStable(P) `` SqStable(Q) `` SqStable(uiff(P;Q)))`

Lemma: sq_stable__all
`∀[A:Type]. ∀[P:A ⟶ ℙ].  ((∀x:A. SqStable(P[x])) `` SqStable(∀x:A. P[x]))`

Lemma: sq_stable__uall
`∀[A:Type]. ∀[P:A ⟶ ℙ].  ((∀[x:A]. SqStable(P[x])) `` SqStable(∀[x:A]. P[x]))`

Lemma: sq_stable__equal
`∀[A:Type]. ∀[x,y:A].  SqStable(x = y ∈ A)`

Lemma: sq_stable__squash
`∀[P:ℙ]. SqStable(↓P)`

Lemma: sq_stable__from_stable
`∀[P:ℙ]. (Stable{P} `` SqStable(P))`

Lemma: sq_stable__not
`∀[P:ℙ]. SqStable(¬P)`

Lemma: sq_stable_from_decidable
`∀[P:ℙ]. (Dec(P) `` SqStable(P))`

Lemma: sq_stable__respects-equality
`∀[A,B:Type].  SqStable(respects-equality(A;B))`

Lemma: uiff_weakening
`∀[P:ℙ]. (SqStable(P) `` {uiff(P;P)})`

Definition: xmiddle
`XM ==  ∀P:ℙ. Dec(P)`

Lemma: xmiddle_wf
`XM ∈ ℙ'`

Definition: weak-xmiddle
`WeakXM ==  ∀P:ℙ. (↓Dec(P))`

Lemma: weak-xmiddle_wf
`WeakXM ∈ ℙ'`

Lemma: xmiddle-implies-stable
`XM `` (∀P:ℙ. Stable{P})`

Lemma: sq_stable_iff_stable
`XM `` (∀P:ℙ. (SqStable(P) `⇐⇒` Stable{P}))`

Lemma: squash_elim
`∀[P:ℙ]. (SqStable(P) `` (↓P `⇐⇒` P))`

Lemma: sq_stable_iff_uimplies
`∀[P:ℙ]. (SqStable(P) `⇐⇒` P supposing P)`

Comment: LOGIC_THMS_tcom
`Theorems of inituitionistic propositional and `
`predicate logic. `

Lemma: dneg_elim
`∀[A:ℙ]. (Dec(A) `` A supposing ¬¬A)`

Lemma: dneg_elim_a
`∀[A:ℙ]. (Dec(A) `` (¬¬A `⇐⇒` A))`

Lemma: iff_symmetry
`∀[A,B:ℙ].  (A `⇐⇒` B `⇐⇒` B `⇐⇒` A)`

Lemma: and_assoc
`∀[A,B,C:ℙ].  (A ∧ B ∧ C `⇐⇒` (A ∧ B) ∧ C)`

Lemma: and_comm
`∀[A,B:ℙ].  (A ∧ B `⇐⇒` B ∧ A)`

Lemma: or_assoc
`∀[A,B,C:ℙ].  (A ∨ B ∨ C `⇐⇒` (A ∨ B) ∨ C)`

Lemma: or_comm
`∀[A,B:ℙ].  (A ∨ B `⇐⇒` B ∨ A)`

Lemma: not_over_or
`∀[A,B:ℙ].  uiff(¬(A ∨ B);(¬A) ∧ (¬B))`

Lemma: not_over_or_a
`∀[A,B:ℙ].  uiff(¬(A ∨ B);{(¬A) ∧ (¬B)})`

Lemma: not_over_and_b
`∀[A,B:ℙ].  ¬(A ∧ B) supposing (¬A) ∨ (¬B)`

Lemma: not_over_and
`∀[A,B:ℙ].  (Dec(A) `` (¬(A ∧ B) `⇐⇒` (¬A) ∨ (¬B)))`

Lemma: not_over_not
`∀[A:ℙ]. (Dec(A) `` (¬¬A `⇐⇒` A))`

Lemma: not_over_implies
`∀[A,B:ℙ].  (¬(A `` B) `⇐⇒` (¬¬A) ∧ (¬B))`

Lemma: and_false_l
`∀[A:Top]. (False ∧ A `⇐⇒` False)`

Lemma: and_false_r
`∀[A:ℙ]. (A ∧ False `⇐⇒` False)`

Lemma: and_true_l
`∀[A:ℙ]. (True ∧ A `⇐⇒` A)`

Lemma: and_true_r
`∀[A:ℙ]. (A ∧ True `⇐⇒` A)`

Lemma: or_false_l
`∀[A:ℙ]. (False ∨ A `⇐⇒` A)`

Lemma: or_false_r
`∀[A:ℙ]. (A ∨ False `⇐⇒` A)`

Lemma: or_true_l
`∀[A:ℙ]. (True ∨ A `⇐⇒` True)`

Lemma: or_true_r
`∀[A:ℙ]. (A ∨ True `⇐⇒` True)`

Lemma: exists_over_and_r
`∀[T:Type]. ∀[A:ℙ]. ∀[B:T ⟶ ℙ].  (∃x:T. (A ∧ B[x]) `⇐⇒` A ∧ (∃x:T. B[x]))`

Lemma: not_over_exists
`∀[T:Type]. ∀[Q:T ⟶ ℙ].  uiff(¬(∃x:T. Q[x]);∀x:T. (¬Q[x]))`

Lemma: not_over_exists_uniform
`∀[T:Type]. ∀[Q:T ⟶ ℙ].  uiff(¬(∃x:T. Q[x]);∀[x:T]. (¬Q[x]))`

Lemma: triple-neg
`∀[A:ℙ]. uiff(¬¬¬A;¬A)`

Lemma: non-uniform-triple-neg
`∀A:ℙ. (¬¬¬A `⇐⇒` ¬A)`

Lemma: minimal-triple-neg
`∀[E:Type]. ∀[A:ℙ].  (((A `` E) `` E) `` E `⇐⇒` A `` E)`

Lemma: triple-neg-ext
`∀[A:ℙ]. uiff(¬¬¬A;¬A)`

Lemma: non-uniform-triple-neg-ext
`∀A:ℙ. (¬¬¬A `⇐⇒` ¬A)`

Lemma: minimal-triple-neg-ext
`∀[E:Type]. ∀[A:ℙ].  (((A `` E) `` E) `` E `⇐⇒` A `` E)`

Comment: EQUALITY_THMS_tcom
`Equality Theorems`

Lemma: equal_symmetry
`∀[T:Type]. ∀[x,y:T].  uiff(x = y ∈ T;y = x ∈ T)`

Comment: REWRITE_SUPPORT_tcom
`Lemma support for rewriting.`

Lemma: iff_transitivity
`∀[P,Q,R:ℙ].  ((P `⇐⇒` Q) `` (Q `⇐⇒` R) `` (P `⇐⇒` R))`

Lemma: implies_transitivity
`∀[P,Q,R:ℙ].  ((P `` Q) `` (Q `` R) `` {P `` R})`

Lemma: and_functionality_wrt_iff
`∀[P1,P2,Q1,Q2:ℙ].  ((P1 `⇐⇒` P2) `` (Q1 `⇐⇒` Q2) `` (P1 ∧ Q1 `⇐⇒` P2 ∧ Q2))`

Lemma: and_functionality_wrt_implies
`∀[P1,P2,Q1,Q2:ℙ].  ({P1 `` P2} `` {Q1 `` Q2} `` {(P1 ∧ Q1) `` (P2 ∧ Q2)})`

Lemma: and_functionality_wrt_uiff2
`∀[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)} `` (Q1 = Q2 ∈ ℙ) `` {P1 ∧ Q1 `⇐⇒` P2 ∧ Q2})`

Lemma: and_functionality_wrt_uiff3
`∀[P1,P2,Q1,Q2:ℙ].  ((P1 = P2 ∈ ℙ) `` {uiff(Q1;Q2)} `` {P1 ∧ Q1 `⇐⇒` P2 ∧ Q2})`

Lemma: implies_functionality_wrt_iff
`∀[P1,P2,Q1,Q2:ℙ].  ({P1 `⇐⇒` P2} `` {Q1 `⇐⇒` Q2} `` {P1 `` Q1 `⇐⇒` P2 `` Q2})`

Lemma: implies_functionality_wrt_implies
`∀[P1,P2,Q1,Q2:ℙ].  ({P1 `` P2} `` {Q1 `` Q2} `` {(P1 `` Q1) `` P2 `` Q2})`

Lemma: decidable_functionality
`∀[P,Q:ℙ].  ((P `⇐⇒` Q) `` (Dec(P) `⇐⇒` Dec(Q)))`

Lemma: iff_functionality_wrt_iff
`∀[P1,P2,Q1,Q2:ℙ].  ((P1 `⇐⇒` P2) `` (Q1 `⇐⇒` Q2) `` (P1 `⇐⇒` Q1 `⇐⇒` P2 `⇐⇒` Q2))`

Lemma: all_functionality_wrt_iff
`∀[S,T:Type]. ∀[P,Q:S ⟶ ℙ].  (∀x:S. (P[x] `⇐⇒` Q[x])) `` (∀x:S. P[x] `⇐⇒` ∀y:T. Q[y]) supposing S = T ∈ Type`

Lemma: all_functionality_wrt_implies
`∀[S,T:Type]. ∀[P,Q:S ⟶ ℙ].  (∀z:S. {P[z] `` Q[z]}) `` {(∀x:S. P[x]) `` (∀y:T. Q[y])} supposing S = T ∈ Type`

Lemma: exists_functionality_wrt_iff
`∀[S,T:Type]. ∀[P,Q:S ⟶ ℙ].  (∀x:S. (P[x] `⇐⇒` Q[x])) `` (∃x:S. P[x] `⇐⇒` ∃y:T. Q[y]) supposing S = T ∈ Type`

Lemma: exists_functionality_wrt_implies
`∀[S,T:Type]. ∀[P,Q:S ⟶ ℙ].  (∀x:S. {P[x] `` Q[x]}) `` {(∃x:S. P[x]) `` (∃y:T. Q[y])} supposing S = T ∈ Type`

Lemma: not_functionality_wrt_iff
`∀[P,Q:ℙ].  {¬P `⇐⇒` ¬Q} supposing P `⇐⇒` Q`

Lemma: not_functionality_wrt_implies
`∀[P,Q:ℙ].  {(¬P) `` (¬Q)} supposing {P `` Q}`

Lemma: or_functionality_wrt_iff
`∀[P1,P2,Q1,Q2:ℙ].  ({P1 `⇐⇒` P2} `` {Q1 `⇐⇒` Q2} `` {P1 ∨ Q1 `⇐⇒` P2 ∨ Q2})`

Lemma: or_functionality_wrt_uiff
`∀[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)} `` {uiff(Q1;Q2)} `` {P1 ∨ Q1 `⇐⇒` P2 ∨ Q2})`

Lemma: or_functionality_wrt_uiff2
`∀[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)} `` (Q1 = Q2 ∈ ℙ) `` {P1 ∨ Q1 `⇐⇒` P2 ∨ Q2})`

Lemma: or_functionality_wrt_uiff3
`∀[P1,P2,Q1,Q2:ℙ].  ((P1 = P2 ∈ ℙ) `` {uiff(Q1;Q2)} `` {P1 ∨ Q1 `⇐⇒` P2 ∨ Q2})`

Lemma: union_functionality_wrt_iff
`∀[P1,P2,Q1,Q2:ℙ].  ({P1 `⇐⇒` P2} `` {Q1 `⇐⇒` Q2} `` {P1 + Q1 `⇐⇒` P2 + Q2})`

Lemma: union_functionality_wrt_uiff
`∀[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)} `` {uiff(Q1;Q2)} `` {P1 + Q1 `⇐⇒` P2 + Q2})`

Lemma: union_functionality_wrt_uiff2
`∀[P1,P2,Q1,Q2:ℙ].  ({uiff(P1;P2)} `` (Q1 = Q2 ∈ ℙ) `` {P1 + Q1 `⇐⇒` P2 + Q2})`

Lemma: union_functionality_wrt_uiff3
`∀[P1,P2,Q1,Q2:ℙ].  ((P1 = P2 ∈ ℙ) `` {uiff(Q1;Q2)} `` {P1 + Q1 `⇐⇒` P2 + Q2})`

Lemma: and-iff
`∀[A:ℙ]. ∀[B,C:⋂a:A. ℙ].  ((A `` (B `⇐⇒` C)) `` {A ∧ B `⇐⇒` A ∧ C})`

Definition: sq_or
`a ↓∨ b ==  ↓a ∨ b`

Lemma: sq_or_wf
`∀[a,b:ℙ].  (a ↓∨ b ∈ ℙ)`

Lemma: sq_stable__sq_or
`∀[a,b:ℙ].  SqStable(a ↓∨ b)`

Lemma: sq_or_simp
`∀[a:ℙ]. ({uiff(a ↓∨ False;↓a)} ∧ {uiff(False ↓∨ a;↓a)} ∧ {uiff(a ↓∨ True;True)} ∧ {uiff(True ↓∨ a;True)})`

Lemma: sq_or_sq_or
`∀[a,b,c:ℙ].  ({uiff(a ↓∨ b ↓∨ c;a ↓∨ (b ∨ c))} ∧ {uiff((b ↓∨ c) ↓∨ a;(b ∨ c) ↓∨ a)})`

Lemma: sq_or_functionality_wrt_iff
`∀[P1,P2,Q1,Q2:ℙ].  ({P1 `⇐⇒` P2} `` {Q1 `⇐⇒` Q2} `` {P1 ↓∨ Q1 `⇐⇒` P2 ↓∨ Q2})`

Lemma: squash_squash
`∀[a:ℙ]. uiff(↓↓a;↓a)`

Lemma: squash_true
`uiff(↓True;True)`

Lemma: squash_false
`uiff(↓False;False)`

Lemma: sq_or_squash
`∀[a,b:ℙ].  uiff((↓a) ↓∨ (↓b);a ↓∨ b)`

Lemma: squash_sq_or
`∀[a,b:ℙ].  uiff(↓a ↓∨ b;a ↓∨ b)`

Lemma: sq_or_squash2
`∀[a,b:ℙ].  uiff((↓a) ↓∨ b;a ↓∨ b)`

Lemma: sq_or_squash3
`∀[a,b:ℙ].  uiff(a ↓∨ (↓b);a ↓∨ b)`

Lemma: squash_and
`∀[a,b:ℙ].  uiff(↓a ∧ b;(↓a) ∧ (↓b))`

Lemma: squash_not
`∀[p:ℙ]. uiff(↓¬p;¬p)`

Lemma: not_squash
`∀[p:ℙ]. uiff(¬↓p;¬p)`

Lemma: squash_equal
`∀[T:Type]. ∀[x,y:T].  uiff(↓x = y ∈ T;x = y ∈ T)`

Lemma: uimplies_functionality_wrt_uiff2
`∀[P,Q1,Q2:ℙ].  ({uiff(Q1;Q2)} `` {uiff(Q1 supposing P;Q2 supposing P)})`

Lemma: uimplies_functionality_wrt_uiff3
`∀[P,Q1,Q2:ℙ].  (Dec(P) `` {uiff(Q1;Q2)} `` {uiff(P supposing Q1;P supposing Q2)})`

Lemma: or_functionality_wrt_implies
`∀[P1,P2,Q1,Q2:ℙ].  ({P1 `` P2} `` {Q1 `` Q2} `` {(P1 ∨ Q1) `` (P2 ∨ Q2)})`

Lemma: squash_functionality_wrt_implies
`∀[P,Q:ℙ].  ({P `` Q} `` {(↓P) `` (↓Q)})`

Lemma: squash_functionality_wrt_iff
`∀[P,Q:ℙ].  ({P `⇐⇒` Q} `` {↓P `⇐⇒` ↓Q})`

Lemma: squash_functionality_wrt_uiff
`∀[P,Q:ℙ].  ({P `⇐⇒` Q} `` {uiff(↓P;↓Q)})`

Lemma: implies_antisymmetry
`∀[P,Q:ℙ].  ((P `` Q) `` (Q `` P) `` (P `⇐⇒` Q))`

Comment: GENERALIZATION_tcom

`⋅`

Lemma: gen_hyp_tp
`∀[A:Type]. ∀[e:A]. ∀[H:A ⟶ 𝕌{j}]. ∀[z:H e].  {{{False `` True}}}`

Comment: MISC_DEFS_com
`Miscellaneous General Definitions`

Definition: let
`let x = a in b[x] ==  (λx.b[x]) a`

Lemma: let_wf
`∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[x:A].  (let v = x in f[v] ∈ B)`

Comment: type_inj_acom
`type_inj is intended chiefly for injecting into quotient`
`types. For convenience, typing lemmas should be proven`
`for each application. e.g. `

`... ∀x:T. [x]{a,b:T//Eab}`

`A general typing lemma for type_inj(x;T) cannot`
`be proven, because it's antecedent would involve the subtype`
`predicate which isn't typeable.`

Definition: type_inj
`[x]{T} ==  x`

Comment: choicef_com
`Hilbert choice operator. Set up for use in theorems where`
`assume_xm abstraction is used outermost. `

`Select the correctly instantiated display form by entering the `
`editor alias "eps". This display form contains variable that`
`is bound by assume_xm.`

`Sequent display routine needs fixing, so that pretty choicef `
`display form is used when XM becomes explicit hypothesis. `

Definition: choicef
`∈x:T. P[x] ==  case xm {y:T| P[y]}  of inl(z) => z | inr(w) => "???"`

Lemma: choicef_wf
`∀[xm:XM]. ∀[T:Type]. ∀[P:T ⟶ ℙ].  ∈x:T. P[x] ∈ T supposing ∃a:T. P[a]`

`∀[A:Type]. ∀[B:A ⟶ Type]. ∀[p:x:A × B[x]]. ∀[C,D:Type]. ∀[f:C ⟶ D]. ∀[b:x:A ⟶ B[x] ⟶ C].`
`  ((f let x,y = p in b[x;y]) = let x,y = p in f b[x;y] ∈ D)`

`∀[A:Type]. ∀[B:A ⟶ Type]. ∀[p:x:A × B[x]]. ∀[C:Type]. ∀[b:x:A ⟶ B[x] ⟶ C].`
`  (let x,y = p in b[x;y] = b[fst(p);snd(p)] ∈ C)`

Definition: singleton
`{a:T} ==  {x:T| x = a ∈ T} `

Lemma: singleton_wf
`∀[T:Type]. ∀[a:T].  ({a:T} ∈ Type)`

Lemma: singleton_properties
`∀[T:Type]. ∀[a:T]. ∀[x:{a:T}].  (x = a ∈ T)`

Definition: unique_set
`{!x:T | P[x]} ==  {x:T| P[x] ∧ (∀y:T. (P[y] `` (y = x ∈ T)))} `

Lemma: unique_set_wf
`∀[T:Type]. ∀[P:T ⟶ ℙ].  ({!x:T | P[x]} ∈ Type)`

Definition: uni_sat
`a = !x:T. Q[x] ==  Q[a] ∧ (∀a':T. (Q[a'] `` (a' = a ∈ T)))`

Lemma: uni_sat_wf
`∀[T:Type]. ∀[a:T]. ∀[Q:T ⟶ ℙ].  (a = !x:T. Q[x] ∈ ℙ)`

Lemma: uni_sat_imp_in_uni_set
`∀[T:Type]. ∀[a:T]. ∀[Q:T ⟶ ℙ].  ((a = !x:T. Q[x]) `` (a ∈ {!x:T | Q[x]}))`

Lemma: sq_stable__uni_sat
`∀[T:Type]. ∀a:T. ∀[Q:T ⟶ ℙ]. ((∀x:T. SqStable(Q[x])) `` SqStable(a = !x:T. Q[x]))`

Lemma: comb_for_pi1_wf
`λA,B,p,z. (fst(p)) ∈ A:Type ⟶ B:(A ⟶ Type) ⟶ p:(a:A × B[a]) ⟶ (↓True) ⟶ A`

Lemma: image-type_wf
`∀[A:Type]. ∀[f:Base].  (Image(A,f) ∈ Type)`

Lemma: int_eq_wf
`∀[T:Type]. ∀[a,b:T]. ∀[x,y:ℤ].  (if x=y then a else b ∈ T)`

Lemma: atom_eq_wf
`∀[T:Type]. ∀[a,b:T]. ∀[x,y:Atom].  (if x=y then a else b fi  ∈ T)`

Lemma: not-0-eq-1
`¬(0 = 1 ∈ ℤ)`

Definition: baseof
`baseof(T) ==  ⋂x:Unit?. case x of inl(z) => T | inr(z) => Base`

Lemma: baseof_wf
`∀[T:Type]. (baseof(T) ∈ Type)`

Lemma: equal-top
`∀[x,y:Top].  (x = y ∈ Top)`

Lemma: equal-unit
`∀[x,y:Unit].  (x = y ∈ Unit)`

Lemma: decidable__squash
`∀[p:ℙ]. (Dec(p) `` Dec(↓p))`

Lemma: squash_thru_implies_dec
`∀[P,Q:ℙ].  uiff(↓P `` Q;P `` (↓Q)) supposing Dec(P)`

Lemma: equality-test
`∀[A,B,C:Type].  ((A = B ∈ Type) `` (C = B ∈ Type) `` (∀[x,y,z:A].  ((x = y ∈ A) `` (z = y ∈ A) `` (x = z ∈ C))))`

Lemma: equality-test2
`∀[A,B,C:Type].`
`  ((A = B ∈ Type)`
`  `` (C = B ∈ Type)`
`  `` (∀[f:A ⟶ A]. ∀[x,y,z,u,w:A].  ((x = (f y) ∈ A) `` (z = (f y) ∈ A) `` (w = u ∈ C) `` (w = z ∈ C) `` (u = x ∈ C))))`

Lemma: or-to-and-by-cases
`∀[X:ℙ]. (Dec(X) `` (∀[P,Q:ℙ].  ((P `` X) `` (Q `` (¬X)) `` {P ∨ Q `⇐⇒` (X `` P) ∧ ((¬X) `` Q)})))`

Definition: exists!
`∃!x:T. P[x] ==  ∃x:T. (P[x] ∧ (∀y:T. (P[y] `` (y = x ∈ T))))`

Lemma: exists!_wf
`∀[T:Type]. ∀[P:T ⟶ ℙ].  (∃!x:T. P[x] ∈ ℙ)`

Lemma: less-member
`∀[T:Type]. ∀[n,m:ℤ]. ∀[a,b:T].  (if (n) < (m)  then a  else b ∈ T)`

Definition: less_than'
`At one time, ⌜a < b⌝ was a primitive type, and the equality rule for it`
`said that ⌜a < b⌝ was a type if ⌜a ∈ ℤ⌝ and ⌜b ∈ ℤ⌝.`
`An elimination rule said that if ⌜t ∈ a < b⌝ then ⌜t ~ Ax⌝.`
`All of these properties are easily derivable if we simply define`
`⌜a < b⌝ using the primitive `less` comparison operator`
`  ⌜if (a) < (b)  then True  else False⌝`
`However, from the fact that ⌜if (a) < (b)  then True  else False⌝ `
`is a proposition (even when we know that it is a true proposition)`
`it does not follow that ⌜a ∈ ℤ⌝ and ⌜b ∈ ℤ⌝ because, for example`
`from  a:⇃({...3}), b:⇃({4...}) we can prove that`
`⌜if (a) < (b)  then True  else False ∈ ℙ⌝.`
`Therefore, we call ⌜if (a) < (b)  then True  else False⌝ ⌜less_than'(a;b)⌝`
`and reserve ⌜a < b⌝ for the proposition that includes ⌜(a ∈ ℤ) ∧ (b ∈ ℤ)⌝⋅`

`less_than'(a;b) ==  if (a) < (b)  then True  else False`

Lemma: less_than'_wf
`∀[a,b:ℤ].  (less_than'(a;b) ∈ ℙ)`

Definition: less_than
`At one time, ⌜a < b⌝ was a primitive type but the properties we need all`
`follow from the definition of ⌜less_than'(a;b)⌝ except for the`
`property that from ⌜a < b⌝ we can derive ⌜(a ∈ ℤ) ∧ (b ∈ ℤ)⌝.`
`So we simply add those to the definition.. `
`⋅`

`a < b ==  ↓less_than'(a;b) ∧ (a ∈ ℤ) ∧ (b ∈ ℤ)`

Lemma: less_than_wf
`∀[a,b:ℤ].  (a < b ∈ ℙ)`

Lemma: istype-less_than
`∀[a,b:ℤ].  istype(a < b)`

Lemma: less_wf
`∀[T:Type]. ∀[a,b:T]. ∀[x,y:ℤ].  (if (x) < (y)  then a  else b ∈ T)`

Lemma: int_subtype_base
`ℤ ⊆r Base`

Lemma: unit_subtype_base
`Unit ⊆r Base`

Lemma: decidable__equal_set
`∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) `` (∀[P:T ⟶ Type]. ∀x,y:{x:T| P[x]} .  Dec(x = y ∈ {x:T| P[x]} )))`

Lemma: decidable__equal_unit
`∀x,y:Unit.  Dec(x = y ∈ Unit)`

Lemma: test-compute-all
`2 * (1 + 2 + 3) ~ 12`

Lemma: minimal-example1
`∀[A,B,X:ℙ].  ((((A `` B) `` X) `` X) `` ((A `` X) `` X) `` (B `` X) `` X)`

Lemma: minimal-example1-ext
`∀[A,B,X:ℙ].  ((((A `` B) `` X) `` X) `` ((A `` X) `` X) `` (B `` X) `` X)`

Lemma: not-not-p-or-not-p
`∀P,A:ℙ.  (((P ∨ (P `` A)) `` A) `` A)`

Lemma: not-not-p-or-not-p-example
`∀P:ℙ. (¬¬(P ∨ (¬P)))`

Lemma: not-not-p-or-not-p-prgram
`∀P,A:ℙ.  (((P ∨ (P `` A)) `` A) `` A)`

Lemma: curry-lemma
`∀A,B,C:ℙ.  (((A ∧ B) `` C) `` A `` B `` C)`

Lemma: curry-lemma-program
`∀A,B,C:ℙ.  (((A ∧ B) `` C) `` A `` B `` C)`

Lemma: minimal-not-not-xmiddle
`∀[P,A:ℙ].  (((P ∨ (P `` A)) `` A) `` A)`

Lemma: not-not-1-xmiddle
`∀[P:ℙ]. (¬¬(P ∨ (¬P)))`

Lemma: minimal-not-not-implies
`∀[P,A:ℙ].  (((((P `` A) `` A) `` (P ∨ A)) `` A) `` A)`

Lemma: minimal-not-not-implies-program
`∀[P,A:ℙ].  (((((P `` A) `` A) `` (P ∨ A)) `` A) `` A)`

Lemma: minimal-not-not-implies-from-program
`∀[P,A:ℙ].  (((((P `` A) `` A) `` (P ∨ A)) `` A) `` A)`

Lemma: example
`∀[P,A:ℙ].  (((P ∨ (P `` A)) `` A) `` A)`

Lemma: minimal-not-not-xmiddle-program
`∀[P,A:ℙ].  (((P ∨ (P `` A)) `` A) `` A)`

Lemma: minimal-not-not-xmiddle-from-program
`∀[P,A:ℙ].  (((P ∨ (P `` A)) `` A) `` A)`

Home Index