Lemma: subtype_rel_dep_function_iff
[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  (uiff(∀[a:C]. (B[a] ⊆D[a]);(a:A ⟶ B[a]) ⊆(c:C ⟶ D[c]))) supposing 
     ((∀x,y:A.  Dec(x y ∈ A)) and 
     (a:A ⟶ B[a]) and 
     (C ⊆A))

Definition: type-continuous
Continuous(T.F[T]) ==  ∀[X:ℕ ⟶ Type]. ((⋂n:ℕF[X n]) ⊆F[⋂n:ℕ(X n)])

Lemma: type-continuous_wf
[F:Type ⟶ Type]. (Continuous(t.F[t]) ∈ ℙ')

Definition: strong-type-continuous
Continuous+(T.F[T]) ==  ∀[X:ℕ ⟶ Type]. ⋂n:ℕF[X n] ≡ F[⋂n:ℕ(X n)]

Lemma: strong-type-continuous_wf
[F:Type ⟶ Type]. (Continuous+(t.F[t]) ∈ ℙ')

Definition: type-monotone
Monotone(T.F[T]) ==  ∀[A,B:Type].  F[A] ⊆F[B] supposing A ⊆B

Lemma: type-monotone_wf
[F:Type ⟶ Type]. (Monotone(T.F[T]) ∈ ℙ')

Lemma: strong-continuous-isect2
[F,G:Type ⟶ Type].  (Continuous+(T.F[T] ⋂ G[T])) supposing (Continuous+(T.G[T]) and Continuous+(T.F[T]))

Definition: continuous-monotone
ContinuousMonotone(T.F[T]) ==  Monotone(T.F[T]) ∧ Continuous(T.F[T])

Lemma: continuous-monotone_wf
[F:Type ⟶ Type]. (ContinuousMonotone(T.F[T]) ∈ ℙ')

Lemma: continuous-monotone-depfunction
[A:Type]. ∀[F:Type ⟶ A ⟶ Type].  ContinuousMonotone(T.a:A ⟶ F[T;a]) supposing ∀a:A. ContinuousMonotone(T.F[T;a])

Lemma: continuous-function
[A,B:Type ⟶ Type].  (Continuous(T.A[T] ⟶ B[T])) supposing (Continuous(T.B[T]) and Continuous+(T.A[T]))

Lemma: strong-continuous-function
[F:Type ⟶ Type]. ∀[A:Type].  Continuous+(T.A ⟶ F[T]) supposing Continuous+(T.F[T])

Lemma: continuous-monotone-function
[F:Type ⟶ Type]. ∀[A:Type]. ContinuousMonotone(T.A ⟶ F[T]) supposing ContinuousMonotone(T.F[T])

Lemma: strong-continuous-product
[F,G:Type ⟶ Type].  (Continuous+(T.F[T] × G[T])) supposing (Continuous+(T.G[T]) and Continuous+(T.F[T]))

Lemma: continuous-monotone-product
[F,G:Type ⟶ Type].
  (ContinuousMonotone(T.F[T] × G[T])) supposing (ContinuousMonotone(T.G[T]) and ContinuousMonotone(T.F[T]))

Lemma: continuous-monotone-depproduct
[F:Type ⟶ Type]. ∀[G:T:Type ⟶ F[T] ⟶ Type].
  (ContinuousMonotone(T.x:F[T] × G[T;x])) supposing 
     ((∀X:ℕ ⟶ Type. ∀x:⋂n:ℕF[X n].  ((⋂n:ℕG[X n;x]) ⊆G[⋂n:ℕ(X n);x])) and 
     (∀A,B:Type.  ((A ⊆B)  (∀x:F[A]. (G[A;x] ⊆G[B;x])))) and 

Lemma: strong-continuous-depproduct
[A:Type]. ∀[G:T:Type ⟶ A ⟶ Type].  Continuous+(T.x:A × G[T;x]) supposing ∀a:A. Continuous+(T.G[T;a])

Lemma: continuous-monotone-set
[A:Type]. ∀[P:A ⟶ ℙ]. ∀[F:Type ⟶ Type].
  (ContinuousMonotone(T.{x:F[T]| P[x]} )) supposing ((∀T:Type. (F[T] ⊆A)) and ContinuousMonotone(T.F[T]))

Lemma: strong-continuous-set
[A:Type]. ∀[P:A ⟶ ℙ]. ∀[F:Type ⟶ Type].
  (Continuous+(T.{x:F[T]| P[x]} )) supposing (Continuous+(T.F[T]) and (∀T:Type. (F[T] ⊆A)))

Lemma: strong-continuous-union
[F,G:Type ⟶ Type].  (Continuous+(T.F[T] G[T])) supposing (Continuous+(T.G[T]) and Continuous+(T.F[T]))

Lemma: b-union-void
[V,T:Type].  ((V ⋃ T) ⊆T) ∧ ((T ⋃ V) ⊆T) supposing ¬V

Lemma: continuous-monotone-union
F,G:Type ⟶ Type.  (ContinuousMonotone(T.F[T])  ContinuousMonotone(T.G[T])  ContinuousMonotone(T.F[T] G[T]))

Lemma: continuous-monotone-isect
[A:Type]. ∀[F:A ⟶ Type ⟶ Type].  ContinuousMonotone(T.⋂a:A. F[a;T]) supposing ∀a:A. ContinuousMonotone(T.F[a;T])

Lemma: continuous-constant
[G:Type]. Continuous+(T.G)

Lemma: continuous-monotone-constant
[G:Type]. ContinuousMonotone(T.G)

Lemma: continuous-id

Lemma: continuous-monotone-id

Definition: union-continuous
union-continuous{i:l}(T.F[T]) ==  ∀[I:Type]. ∀[X:I ⟶ Type].  (⋃n:I.F[X n] ⊆F[⋃n:I.(X n)])

Lemma: union-continuous_wf
[F:Type ⟶ Type]. (union-continuous{i:l}(T.F[T]) ∈ ℙ')

Lemma: type-monotone-union-continuous
[F:Type ⟶ Type]. union-continuous{i:l}(T.F[T]) supposing Monotone(T.F[T])

Lemma: union-continuous-type-monotone
[F:Type ⟶ Type]. (Monotone(T.F[T])) supposing (union-continuous{i:l}(T.F[T]) and (∀A,B:Type.  (A ≡  F[A] ≡ F[B])))

Lemma: int_sq

Lemma: nat_sq

Lemma: atom_sq

Lemma: eq_atom_eq_false_elim_sqequal
[x,y:Atom].  ¬(x y ∈ Atom) supposing =a ff

Lemma: eq_atom_eq_true_elim_sqequal
[x,y:Atom].  y ∈ Atom supposing =a tt

Lemma: lt_int_eq_false_elim_sqequal
[i,j:ℤ].  ¬i < supposing i <ff

Lemma: lt_int_eq_true_elim_sqequal
[i,j:ℤ].  i < supposing i <tt

Lemma: eq_int_eq_false_elim_sqequal
[i,j:ℤ].  i ≠ supposing (i =z j) ff

Lemma: eq_int_eq_true_elim_sqequal
[i,j:ℤ].  j ∈ ℤ supposing (i =z j) tt

Lemma: uimplies_subtype
[A,B:Type]. ∀[P:ℙ].  (A supposing P ⊆B) supposing ((A ⊆B) and P)

Lemma: isect_subtype
[A1:Type]. ∀[B1:A1 ⟶ ℙ]. ∀[A2:Type]. ∀[B2:A2 ⟶ ℙ].
  ((⋂x:A1. B1[x]) ⊆(⋂x:A2. B2[x])) supposing ((∀x:A2. (B1[x] ⊆B2[x])) and (A2 ⊆A1))

Lemma: equal_subtype
[A,B:Type]. ∀[a1,a2:A]. ∀[b1,b2:B].  (a1 a2 ∈ A) ⊆(b1 b2 ∈ B) supposing (a1 a2 ∈ A)  (b1 b2 ∈ B)

Lemma: bunion-value-type
[A,B:Type].  (value-type(A ⋃ B)) supposing (value-type(B) and value-type(A))

Lemma: bunion-valueall-type
[A,B:Type].  (valueall-type(A ⋃ B)) supposing (valueall-type(B) and valueall-type(A))

Lemma: isect2_functionality_wrt_subtype_rel
[A1,B1,A2,B2:Type].  (A1 ⋂ B1 ⊆A2 ⋂ B2) supposing ((A1 ⊆A2) and (B1 ⊆B2))

Lemma: equal-in-subtype-implies
[A,B:Type]. ∀[x,y:A].  (x y ∈ B) supposing ((x y ∈ A) and (A ⊆B))

Lemma: function-subtype-top
[A,B:Type].  ((A ⟶ B) ⊆Top)

Lemma: top-subtype-function
[A,B:Type].  Top ⊆(A ⟶ B) supposing ¬A

Definition: strong-subtype
strong-subtype(A;B) ==  (A ⊆B) c∧ ({b:B| ∃a:A. (b a ∈ B)}  ⊆A)

Lemma: strong-subtype_wf
[A,B:Type].  (strong-subtype(A;B) ∈ ℙ)

Lemma: strong-subtype-iff-respects-equality
[A,B:Type].  uiff(strong-subtype(A;B);(A ⊆B) ∧ respects-equality(B;A))

Lemma: strong-subtype-iff-preserves-singleton
[A,B:Type].  uiff(strong-subtype(A;B);(A ⊆B) ∧ (∀a:A. ({a:B} ⊆{a:A})))

Lemma: strong-subtype-implies
[A,B:Type].  (strong-subtype(A;B)  {∀b:B. ∀a:A.  ((b a ∈ B)  (b a ∈ A))})

Lemma: strong-subtype_witness
[A,B:Type].  (strong-subtype(A;B)  (<Ax, Ax> ∈ strong-subtype(A;B)))

Lemma: strong-subtype-self
[A:Type]. strong-subtype(A;A)

Lemma: strong-subtype-equal
[A,B:Type].  strong-subtype(A;B) supposing B ∈ Type

Lemma: strong-subtype-ext-equal
[A,B:Type].  (strong-subtype(A;B)) supposing ((A ⊆B) and (B ⊆A))

Lemma: strong-subtype_transitivity
[A,B,C:Type].  (strong-subtype(A;C)) supposing (strong-subtype(B;C) and strong-subtype(A;B))

Lemma: strong-subtype_functionality
[A1,B1,A2,B2:Type].  (A1 ≡ A2  B1 ≡ B2  strong-subtype(A1;B1)  strong-subtype(A2;B2))

Lemma: strong-subtype-void
[T:Type]. strong-subtype(Void;T)

Lemma: strong-subtype-set
[A,B:Type].  ∀[P:A ⟶ ℙ]. ∀[Q:B ⟶ ℙ].  strong-subtype({x:A| P[x]} ;{x:B| Q[x]} supposing ∀x:A. (P[x]  Q[x]) suppos\000Cing strong-subtype(A;B)

Lemma: strong-subtype-set1
[A:Type]. ∀[P,Q:A ⟶ ℙ].  strong-subtype({x:A| P[x]} ;{x:A| Q[x]} supposing ∀x:A. (P[x]  Q[x])

Lemma: strong-subtype-set2
[A:Type]. ∀[P:A ⟶ ℙ].  strong-subtype({x:A| P[x]} ;A)

Lemma: strong-subtype-set3
[A,B:Type]. ∀[P:A ⟶ ℙ].  strong-subtype({x:A| P[x]} ;B) supposing strong-subtype(A;B)

Lemma: strong-subtype-product
[A,B,C,D:Type].  (strong-subtype(A × B;C × D)) supposing (strong-subtype(B;D) and strong-subtype(A;C))

Lemma: strong-subtype-dep-product
[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  (strong-subtype(a:A × B[a];c:C × D[c])) supposing ((∀a:A. strong-subtype(B[a];D[a])) and strong-subtype(A;C))

Lemma: strong-subtype-union
[A,B,C,D:Type].  (strong-subtype(A B;C D)) supposing (strong-subtype(B;D) and strong-subtype(A;C))

Lemma: strong-subtype-eq1
[A,B:Type]. ∀[b:B]. ∀[a:A].  ((b ∈ A) c∧ (b a ∈ A)) supposing ((b a ∈ B) and strong-subtype(A;B))

Lemma: strong-subtype-eq2
[A,B:Type]. ∀[b:B]. ∀[a:A].  (b a ∈ A) supposing ((b a ∈ B) and strong-subtype(A;B))

Lemma: strong-subtype-eq3
[A,B:Type]. ∀[b:B]. ∀[a:A].  {b a ∈ supposing a ∈ B} supposing strong-subtype(A;B)

Lemma: strong-subtype-eq4
[A,B:Type]. ∀[b:B]. ∀[a:A].  {b a ∈ supposing a ∈ A} supposing strong-subtype(B;A)

Lemma: strong-subtype-member
[A,B:Type]. ∀[b:B]. ∀[a:A].  {b ∈ supposing a ∈ B} supposing strong-subtype(A;B)

Lemma: singleton-subtype
[A,B:Type].  ∀[a:A]. ({z:B| a ∈ B}  ⊆A) supposing strong-subtype(A;B)

Lemma: inject-subtype
[C,A:Type].  ∀[B:Type]. ∀[f:A ⟶ B].  Inj(C;B;f) supposing Inj(A;B;f) supposing strong-subtype(C;A)

Lemma: b-union-equality-disjoint
A,B:Type. ∀a:A. ∀b:B.  ((¬A ⋂ B)  (a b ∈ (A ⋃ B))))

Lemma: b-union-equality-disjoint2
A,B:Type. ∀a:A. ∀b:B.  ((a b ∈ (A ⋃ B))  (¬¬A ⋂ B))

Lemma: strong-subtype-b-union-better
[A,B:Type].  strong-subtype(A;A ⋃ B) supposing strong-subtype(A ⋂ B;B)

Lemma: strong-subtype-isect-base
[A:Type]. (strong-subtype(A ⋂ Base;Base) ∧ strong-subtype(Base ⋂ A;Base))

Lemma: strong-subtype-union-base
[A:Type]. (strong-subtype(A;A ⋃ Base) ∧ strong-subtype(A;Base ⋃ A))

Lemma: b-union-base-equality
A:Type. ∀a,b:Base.  ((a b ∈ (Base ⋃ A))  (b ∈ A)  (a b ∈ A))

Lemma: strong-subtype-b-union
[A,B:Type].  strong-subtype(A;A ⋃ B) ∧ strong-subtype(B;A ⋃ B) supposing ¬A ⋂ B

Lemma: isect2-b-union-subtype
[A,B,C:Type].  A ⋂ B ⋃ C ⊆(A ⋂ B ⋃ A ⋂ C) supposing ¬B ⋂ C

Lemma: strong-continuous-b-union
[F,G:Type ⟶ Type].
  (Continuous+(T.F[T] ⋃ G[T])) supposing ((∀T,S:Type.  F[T] ⋂ G[S])) and Continuous+(T.G[T]) and Continuous+(T.F[T]))

Lemma: inject_functionality
[A,B,C:Type]. ∀[f:B ⟶ C].  (Inj(A;C;f)) supposing (Inj(B;C;f) and strong-subtype(A;B))

Lemma: sq_stable__strong-subtype
[A,B:Type].  SqStable(strong-subtype(A;B))

Lemma: id-fun-subtype
[A,B:Type].  id-fun(B) ⊆id-fun(A) supposing strong-subtype(A;B)

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

Lemma: subtype_by_equality
[A,B:Type].  ((∀x,y:Base.  ((x y ∈ A)  (x y ∈ B)))  (A ⊆B))

Definition: per-class
per-class(T;a) ==  {x:Base| a ∈ T} 

Lemma: per-class_wf
[T:Type]. ∀[a:Base ⋃ T].  (per-class(T;a) ∈ Type)

Lemma: trivial-per-class
[T:Type]. ∀[a:T ⋂ Base].  (a ∈ per-class(T;a))

Lemma: squash-per-class
[T:Type]. ∀[a:T].  (↓per-class(T;a))

Lemma: subtype_rel_per-class
[A,B:Type].  ∀[a:A]. (per-class(A;a) ⊆per-class(B;a)) supposing A ⊆B

Lemma: per-class-subtype-singleton
[T:Type]. ∀[a:T].  (per-class(T;a) ⊆{x:T| a ∈ T} )

Lemma: per-class-base-singleton
[T:Type]. ∀[a:T].  per-class(T;a) ≡ Base ⋂ {x:T| a ∈ T} 

Lemma: per-class-base
[T:Type]. ∀[a:T]. ∀[b:per-class(T;a)].  (b a) supposing T ⊆Base

Definition: t-sqle
t-sqle(T;a;b) ==  ↓∃a':per-class(T;a). ∃b':per-class(T;b). (a' ≤ b')

Lemma: t-sqle_wf
[T:Type]. ∀[a,b:T].  (t-sqle(T;a;b) ∈ ℙ)

Lemma: sq_stable__t-sqle
[T:Type]. ∀[a,b:T].  SqStable(t-sqle(T;a;b))

Lemma: t-sqle_reflexive
[T:Type]. ∀a:T. t-sqle(T;a;a)

Lemma: t-sqle-subtype
[A,B:Type].  ∀[a,b:A].  (t-sqle(A;a;b)  t-sqle(B;a;b)) supposing A ⊆B

Lemma: t-sqle-apply
[A,B:Type].  ∀a1,a2:A. ∀f1,f2:a:A ⟶ B.  (t-sqle(a:A ⟶ B;f1;f2)  t-sqle(A;a1;a2)  t-sqle(B;f1 a1;f2 a2))

Lemma: t-sqle-base
[T:Type]. ∀a,b:T.  (t-sqle(T;a;b)  (a ≤ b)) supposing T ⊆Base

Definition: is-above
is-above(T;a;z) ==  ∃y:Base. ((y a ∈ T) ∧ (y ≤ z))

Lemma: is-above_wf
[T:Type]. ∀[a:T]. ∀[z:Base].  (is-above(T;a;z) ∈ ℙ)

Lemma: is-above-subtype
[A,B:Type].  ∀[a:A]. ∀[z:Base].  (is-above(A;a;z)  is-above(B;a;z)) supposing A ⊆B

Lemma: is-above-singleton-subtype
[A:Type]. ∀[a:A]. ∀[B:Type].  ∀[z:Base]. (is-above(A;a;z)  is-above(B;a;z)) supposing {x:A| a ∈ A}  ⊆B

Lemma: is-above-int
[n:ℤ]. ∀[z:Base].  n ∈ ℤ supposing is-above(ℤ;n;z)

Lemma: is-above-axiom-general
[T:Type]. ∀[z:Base]. Ax supposing is-above(T;Ax;z) supposing T ⊆Base

Lemma: is-above-axiom
[z:Base]. Ax supposing is-above(Unit;Ax;z)

Lemma: is-above-pair
[A:Type]. ∀[B:A ⟶ Type]. ∀[a:A]. ∀[b:B[a]].
  ∀z:Base. (is-above(a:A × B[a];<a, b>;z)  (∃c,d:Base. ((z ~ <c, d>) ∧ is-above(A;a;c) ∧ is-above(B[a];b;d))))

Lemma: is-above-inl
[A,B:Type]. ∀[a:A].  ∀z:Base. (is-above(A B;inl a;z)  (∃c:Base. ((z inl c) ∧ is-above(A;a;c))))

Lemma: is-above-inr
[A,B:Type]. ∀[a:B].  ∀z:Base. (is-above(A B;inr ;z)  (∃c:Base. ((z inr ) ∧ is-above(B;a;c))))

Definition: mono
mono(T) ==  ∀a:T. ∀b:Base.  (is-above(T;a;b)  (a b ∈ T))

Lemma: mono_wf
[T:Type]. (mono(T) ∈ ℙ)

Lemma: t-sqle-apply-dependent
  ∀[B:A ⟶ Type]
    ∀a1,a2:A. ∀f1,f2:a:A ⟶ B[a].  (t-sqle(a:A ⟶ B[a];f1;f2)  t-sqle(A;a1;a2)  t-sqle(B[a1];f1 a1;f2 a2)) 
  supposing mono(A)

Lemma: int-mono

Lemma: unit-mono

Lemma: void-mono

Lemma: subtype-mono
[A,B:Type].  (mono(A)) supposing (mono(B) and strong-subtype(A;B))

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

Lemma: nat-mono

Lemma: pair-mono
A:Type. ∀B:A ⟶ Type.  ((mono(A) ∧ (∀a:A. mono(B[a])))  mono(a:A × B[a]))

Lemma: function-mono
A:Type. ∀B:A ⟶ Type.  (((A ⊆Base) ∧ (∀a:A. mono(B[a])) ∧ (↓∃a:A. value-type(B[a])))  mono(a:A ⟶ B[a]))

Lemma: isect-mono
A:Type. ∀B:A ⟶ Type.  ((∀a:A. mono(B[a]))  mono(⋂a:A. B[a]))

Lemma: union-mono
A,B:Type.  ((mono(A) ∧ mono(B))  mono(A B))

Lemma: bool-mono

Lemma: sqle-mono-implies-equal
[T:Type]. ∀[x,y:Base].  (x y ∈ T) supposing ((x ∈ T) and (x ≤ y)) supposing mono(T)

Lemma: squash-exists-is-union-squash
[T:Type]. ∀[P:T ⟶ ℙ].  ↓∃x:T. P[x] ≡ ⋃x:T.(↓P[x])

Lemma: squash-product
[A,B:Type].  uiff(↓A × B;↓A × (↓B))

Lemma: union-set-is-set-exists
[A,B:Type]. ∀[P:A ⟶ B ⟶ ℙ].  ⋃x:A.{y:B| P[x;y]}  ≡ {y:B| ∃x:A. P[x;y]} 

Lemma: prod-image-is-image
[A:Type]. ∀[f:Base]. ∀[B:Image(A,f) ⟶ Type]. ∀[g:Base].
  y:Image(A,f) × Image(B[y],g) ≡ Image((z:A × B[f z]),(λp.let a,b 
                                                          in <a, b>))

Lemma: squash-union-is-union-squash
[A:Type]. ∀[P:A ⟶ Type].  ↓⋃a:A.P[a] ≡ ⋃a:A.(↓P[a])

Lemma: subtype-iff-id-mem-fun
[A,B:Type].  uiff(A ⊆B;λx.x ∈ A ⟶ B)

Lemma: type-monotone_fun_exp_top
[F:Type ⟶ Type]. ∀[n,m:ℕ].  (F^n Top) ⊆(F^m Top) supposing m ≤ supposing Monotone(T.F[T])

Lemma: type-monotone-fun_exp
[F:Type ⟶ Type]. ∀[n,m:ℕ].  (F^n Void) ⊆(F^m Void) supposing n ≤ supposing Monotone(T.F[T])

Definition: exception-name
exception-name(e;n) ==  isaxiom(e?n:x.Ax) ∧b isint(e?n:x.2)

Lemma: exception-name_wf
[n:Atom2]. ∀[t:Value() ⋃ Exception(n;Top)].  (exception-name(t;n) ∈ 𝔹)

Lemma: assert-exception-name
[n:Atom2]. ∀[t:Value() ⋃ Exception(n;Top)].
  (t ∈ Exception(n;Top) supposing ↑exception-name(t;n) ∧ t ∈ Value() supposing ¬↑exception-name(t;n))

Definition: set-axiom-of-choice
If we think of "sets" as types, then family of non-empty sets is
given by an "index set" and function S ∈ T ⟶ Type such that
x:T. (S x).  The condition ∀x:T. (S x) says that each "set" is inhabited.

Now, the constructive interpretation of ∀x:T. (S x) is function of type ⌜x:T ⟶ (S x)⌝
so one version of the axiom of choice is necessarily true.

But, if we require "function" from the family of sets to members of those
sets, then the function must be extensional. That would mean that
when two sets and are extensionally the same set then the function
must choose the same value for that it chooses for x.

We define here the statement of an axiom of choice that says that such
an extensional choice function exists. Instead of extensional equality of sets
we use extensional equality of types.

Following Diaconescu (or Goodman-Myhill) we can prove that this
version of AC implies the law of excluded middle
And therefore, it is proveably false in Nuprl
(Error :set-axiom-of-choice-is-false).⋅

Set-AC ==  ∀T:Type. ∀S:T ⟶ Type.  ((∀x:T. (S x))  (∃f:x:T ⟶ (S x). ∀x,y:T.  (S x ≡  ((f x) (f y) ∈ (S x)))))

Lemma: set-axiom-of-choice_wf
Set-AC ∈ ℙ'

Lemma: set-axiom-of-choice-implies-xmiddle
Set-AC  (∀P:ℙ((↓P) ∨ P)))

Lemma: subtype-TYPE
Type ⊆TYPE

Home Index