A : eta {|prop|type|} => {|Pure.prop_def|axiom|} A
{|'a|} : Typ => x : eta {|'a|} => {|Pure.term_def|axiom|} {|'a|} x
{|'a|} : Typ => {|Pure.sort_constraint_def|axiom|} {|'a|}
A : eta {|prop|type|} => B : eta {|prop|type|} => {|Pure.conjunction_def|axiom|} A B
A : eta {|prop|type|} => {|Pure.equal_elim|axiom|} A ({|Pure.prop|const|} A) ({|Pure.symmetric|axiom|} {|prop|type|} ({|Pure.prop|const|} A) A ({|Pure.prop_def|axiom|} A))
A : eta {|prop|type|} => {|Pure.equal_elim|axiom|} ({|Pure.prop|const|} A) A ({|Pure.prop_def|axiom|} A)
{|'a|} : Typ => x : eta {|'a|} => {|Pure.equal_elim|axiom|} ({|Pure.all|const|} {|prop|type|} (A : eta {|prop|type|} => {|Pure.imp|const|} A A)) ({|Pure.term|const|} {|'a|} x) ({|Pure.symmetric|axiom|} {|prop|type|} ({|Pure.term|const|} {|'a|} x) ({|Pure.all|const|} {|prop|type|} (A : eta {|prop|type|} => {|Pure.imp|const|} A A)) ({|Pure.term_def|axiom|} {|'a|} x)) (A : eta {|prop|type|} => H : eps A => H)
{|'a|} : Typ => x : eta {|'a|} => {|Pure.equal_elim|axiom|} ({|Pure.all|const|} {|prop|type|} (A : eta {|prop|type|} => {|Pure.imp|const|} A A)) ({|Pure.term|const|} {|'a|} x) ({|Pure.symmetric|axiom|} {|prop|type|} ({|Pure.term|const|} {|'a|} x) ({|Pure.all|const|} {|prop|type|} (A : eta {|prop|type|} => {|Pure.imp|const|} A A)) ({|Pure.term_def|axiom|} {|'a|} x)) (A : eta {|prop|type|} => H : eps A => H)
{|'a|} : Typ => x : eta {|'a|} => proof628 {|'a|} x
{|'a|} : Typ => x : eta {|'a|} => proof630 {|'a|} x
{|'a|} : Typ => {|Pure.equal_elim|axiom|} ({|Pure.term|const|} ({|itself|type|} {|'a|}) ({|Pure.type|const|} {|'a|})) ({|Pure.sort_constraint|const|} {|'a|} ({|Pure.type|const|} {|'a|})) ({|Pure.symmetric|axiom|} {|prop|type|} ({|Pure.sort_constraint|const|} {|'a|} ({|Pure.type|const|} {|'a|})) ({|Pure.term|const|} ({|itself|type|} {|'a|}) ({|Pure.type|const|} {|'a|})) ({|Pure.sort_constraint_def|axiom|} {|'a|})) ({|Pure.termI|thm|} ({|itself|type|} {|'a|}) ({|Pure.type|const|} {|'a|}))
{|'a|} : Typ => {|Pure.equal_elim|axiom|} ({|Pure.term|const|} ({|itself|type|} {|'a|}) ({|Pure.type|const|} {|'a|})) ({|Pure.sort_constraint|const|} {|'a|} ({|Pure.type|const|} {|'a|})) ({|Pure.symmetric|axiom|} {|prop|type|} ({|Pure.sort_constraint|const|} {|'a|} ({|Pure.type|const|} {|'a|})) ({|Pure.term|const|} ({|itself|type|} {|'a|}) ({|Pure.type|const|} {|'a|})) ({|Pure.sort_constraint_def|axiom|} {|'a|})) (proof632 ({|itself|type|} {|'a|}) ({|Pure.type|const|} {|'a|}))
{|'a|} : Typ => proof640 {|'a|}
{|'a|} : Typ => proof642 {|'a|}
{|'a|} : Typ => A : eta {|prop|type|} => {|Pure.equal_intr|axiom|} ({|Pure.imp|const|} ({|Pure.sort_constraint|const|} {|'a|} ({|Pure.type|const|} {|'a|})) A) A (H : eps ({|Pure.imp|const|} ({|Pure.sort_constraint|const|} {|'a|} ({|Pure.type|const|} {|'a|})) A) => H ({|Pure.sort_constraintI|thm|} {|'a|})) (H : eps A => Ha : eps ({|Pure.sort_constraint|const|} {|'a|} ({|Pure.type|const|} {|'a|})) => H)
A : eta {|prop|type|} => B : eta {|prop|type|} => H : eps ({|Pure.conjunction|const|} A B) => {|Pure.equal_elim|axiom|} ({|Pure.conjunction|const|} A B) ({|Pure.all|const|} {|prop|type|} (C : eta {|prop|type|} => {|Pure.imp|const|} ({|Pure.imp|const|} A ({|Pure.imp|const|} B C)) C)) ({|Pure.conjunction_def|axiom|} A B) H A (Ha : eps A => Hb : eps B => Ha)
A : eta {|prop|type|} => B : eta {|prop|type|} => H : eps ({|Pure.conjunction|const|} A B) => {|Pure.equal_elim|axiom|} ({|Pure.conjunction|const|} A B) ({|Pure.all|const|} {|prop|type|} (C : eta {|prop|type|} => {|Pure.imp|const|} ({|Pure.imp|const|} A ({|Pure.imp|const|} B C)) C)) ({|Pure.conjunction_def|axiom|} A B) H B (Ha : eps A => Hb : eps B => Hb)
A : eta {|prop|type|} => B : eta {|prop|type|} => H : eps A => Ha : eps B => {|Pure.equal_elim|axiom|} ({|Pure.all|const|} {|prop|type|} (C : eta {|prop|type|} => {|Pure.imp|const|} ({|Pure.imp|const|} A ({|Pure.imp|const|} B C)) C)) ({|Pure.conjunction|const|} A B) ({|Pure.symmetric|axiom|} {|prop|type|} ({|Pure.conjunction|const|} A B) ({|Pure.all|const|} {|prop|type|} (C : eta {|prop|type|} => {|Pure.imp|const|} ({|Pure.imp|const|} A ({|Pure.imp|const|} B C)) C)) ({|Pure.conjunction_def|axiom|} A B)) (C : eta {|prop|type|} => Hb : eps ({|Pure.imp|const|} A ({|Pure.imp|const|} B C)) => Hb H Ha)
P : eta {|prop|type|} => Q : eta {|prop|type|} => H : eps ({|Pure.imp|const|} P Q) => H
A : eta {|prop|type|} => {|Pure.equal_elim|axiom|} A ({|Pure.prop|const|} A) ({|Pure.symmetric|axiom|} {|prop|type|} ({|Pure.prop|const|} A) A ({|Pure.prop_def|axiom|} A))
A : eta {|prop|type|} => proof598 A
A : eta {|prop|type|} => proof600 A
A : eta {|prop|type|} => {|Pure.equal_elim|axiom|} ({|Pure.prop|const|} A) A ({|Pure.prop_def|axiom|} A)
A : eta {|prop|type|} => proof610 A
A : eta {|prop|type|} => proof612 A
P : eta {|prop|type|} => Q : eta {|prop|type|} => H : eps ({|Pure.imp|const|} P Q) => H
P : eta {|prop|type|} => H : eps P => H
P : eta {|prop|type|} => Q : eta {|prop|type|} => H : eps P => Ha : eps ({|Pure.imp|const|} P Q) => proof602 Q (proof41928 P Q Ha (proof41930 P H))
P : eta {|prop|type|} => Q : eta {|prop|type|} => H : eps ({|Pure.imp|const|} P Q) => Ha : eps P => proof614 Q (proof41932 P Q Ha H)
P : eta {|prop|type|} => Q : eta {|prop|type|} => proof41934 P Q
P : eta {|prop|type|} => V : eta {|prop|type|} => W : eta {|prop|type|} => H : eps ({|Pure.imp|const|} P V) => Ha : eps P => Hb : eps ({|Pure.imp|const|} V W) => Hb ({|Pure.meta_mp|thm|} P V H Ha)
{|'a|} : Typ => P : eta ({|fun|type|} {|'a|} {|prop|type|}) => x : eta {|'a|} => H : eps ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => P x)) => H x
{|'a|} : Typ => P : eta ({|fun|type|} {|'a|} {|prop|type|}) => H : eps ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => P x)) => H
{|'a|} : Typ => P : eta ({|fun|type|} {|'a|} {|prop|type|}) => x : eta {|'a|} => H : eps ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => P x)) => proof602 (P x) (proof42020 {|'a|} P H x)
{|'a|} : Typ => P : eta ({|fun|type|} {|'a|} {|prop|type|}) => x : eta {|'a|} => H : eps ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => P x)) => proof614 (P x) (proof42022 {|'a|} P x H)
{|'a|} : Typ => P : eta ({|fun|type|} {|'a|} {|prop|type|}) => x : eta {|'a|} => proof42024 {|'a|} P x
{|'a|} : Typ => P : eta ({|fun|type|} {|'a|} {|prop|type|}) => x : eta {|'a|} => W : eta {|prop|type|} => H : eps ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => P x)) => Ha : eps ({|Pure.imp|const|} (P x) W) => Ha ({|Pure.meta_spec|thm|} {|'a|} P x H)
{|'a|} : Typ => {|'b|} : Typ => P : eta ({|fun|type|} {|'a|} ({|fun|type|} {|'b|} {|prop|type|})) => {|Pure.equal_intr|axiom|} ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => {|Pure.all|const|} {|'b|} (y : eta {|'b|} => (xa : eta {|'a|} => ya : eta {|'b|} => (xb : eta {|'a|} => yb : eta {|'b|} => (xc : eta {|'a|} => yc : eta {|'b|} => P xc yc) xb yb) xa ya) x y))) ({|Pure.all|const|} {|'b|} (y : eta {|'b|} => {|Pure.all|const|} {|'a|} (x : eta {|'a|} => (xa : eta {|'a|} => ya : eta {|'b|} => (xb : eta {|'a|} => yb : eta {|'b|} => (xc : eta {|'a|} => yc : eta {|'b|} => P xc yc) xb yb) xa ya) x y))) (H : eps ({|Pure.all|const|} {|'a|} (a : eta {|'a|} => {|Pure.all|const|} {|'b|} (y : eta {|'b|} => (x : eta {|'a|} => ya : eta {|'b|} => (xa : eta {|'a|} => yb : eta {|'b|} => (xb : eta {|'a|} => yc : eta {|'b|} => P xb yc) xa yb) x ya) a y))) => y : eta {|'b|} => x : eta {|'a|} => H x y) (H : eps ({|Pure.all|const|} {|'b|} (a : eta {|'b|} => {|Pure.all|const|} {|'a|} (x : eta {|'a|} => (xa : eta {|'a|} => y : eta {|'b|} => (xb : eta {|'a|} => ya : eta {|'b|} => (xc : eta {|'a|} => yb : eta {|'b|} => P xc yb) xb ya) xa y) x a))) => x : eta {|'a|} => y : eta {|'b|} => H y x)
A : eta {|prop|type|} => B : eta {|prop|type|} => H : eps ({|Pure.conjunction|const|} A B) => {|Pure.equal_elim|axiom|} ({|Pure.conjunction|const|} A B) ({|Pure.all|const|} {|prop|type|} (C : eta {|prop|type|} => {|Pure.imp|const|} ({|Pure.imp|const|} A ({|Pure.imp|const|} B C)) C)) ({|Pure.conjunction_def|axiom|} A B) H A (Ha : eps A => Hb : eps B => Ha)
A : eta {|prop|type|} => B : eta {|prop|type|} => proof696 A B
A : eta {|prop|type|} => B : eta {|prop|type|} => proof698 A B
A : eta {|prop|type|} => B : eta {|prop|type|} => H : eps ({|Pure.conjunction|const|} A B) => {|Pure.equal_elim|axiom|} ({|Pure.conjunction|const|} A B) ({|Pure.all|const|} {|prop|type|} (C : eta {|prop|type|} => {|Pure.imp|const|} ({|Pure.imp|const|} A ({|Pure.imp|const|} B C)) C)) ({|Pure.conjunction_def|axiom|} A B) H B (Ha : eps A => Hb : eps B => Hb)
A : eta {|prop|type|} => B : eta {|prop|type|} => proof708 A B
A : eta {|prop|type|} => B : eta {|prop|type|} => proof710 A B
A : eta {|prop|type|} => B : eta {|prop|type|} => H : eps A => Ha : eps B => {|Pure.equal_elim|axiom|} ({|Pure.all|const|} {|prop|type|} (C : eta {|prop|type|} => {|Pure.imp|const|} ({|Pure.imp|const|} A ({|Pure.imp|const|} B C)) C)) ({|Pure.conjunction|const|} A B) ({|Pure.symmetric|axiom|} {|prop|type|} ({|Pure.conjunction|const|} A B) ({|Pure.all|const|} {|prop|type|} (C : eta {|prop|type|} => {|Pure.imp|const|} ({|Pure.imp|const|} A ({|Pure.imp|const|} B C)) C)) ({|Pure.conjunction_def|axiom|} A B)) (C : eta {|prop|type|} => Hb : eps ({|Pure.imp|const|} A ({|Pure.imp|const|} B C)) => Hb H Ha)
A : eta {|prop|type|} => B : eta {|prop|type|} => proof720 A B
A : eta {|prop|type|} => B : eta {|prop|type|} => proof722 A B
{|'a|} : Typ => A : eta ({|fun|type|} {|'a|} {|prop|type|}) => B : eta ({|fun|type|} {|'a|} {|prop|type|}) => {|Pure.equal_intr|axiom|} ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => {|Pure.conjunction|const|} ((xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => A xc) xb) xa) x) ((xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => B xc) xb) xa) x))) ({|Pure.conjunction|const|} ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => (xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => A xc) xb) xa) x)) ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => (xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => B xc) xb) xa) x))) (H : eps ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => {|Pure.conjunction|const|} ((xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => A xc) xb) xa) x) ((xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => B xc) xb) xa) x))) => {|Pure.conjunctionI|thm|} ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => (xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => A xc) xb) xa) x)) ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => (xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => B xc) xb) xa) x)) (x : eta {|'a|} => {|Pure.conjunctionD1|thm|} ((xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => A xc) xb) xa) x) ((xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => B xc) xb) xa) x) (H x)) (x : eta {|'a|} => {|Pure.conjunctionD2|thm|} ((xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => A xc) xb) xa) x) ((xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => B xc) xb) xa) x) (H x))) (H : eps ({|Pure.conjunction|const|} ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => (xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => A xc) xb) xa) x)) ({|Pure.all|const|} {|'a|} (x : eta {|'a|} => (xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => B xc) xb) xa) x))) => x : eta {|'a|} => {|Pure.conjunctionI|thm|} ((xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => A xc) xb) xa) x) ((xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => B xc) xb) xa) x) ({|Pure.conjunctionD1|thm|} ({|Pure.all|const|} {|'a|} (xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => (xd : eta {|'a|} => A xd) xc) xb) xa)) ({|Pure.all|const|} {|'a|} (xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => (xd : eta {|'a|} => B xd) xc) xb) xa)) H x) ({|Pure.conjunctionD2|thm|} ({|Pure.all|const|} {|'a|} (xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => (xd : eta {|'a|} => A xd) xc) xb) xa)) ({|Pure.all|const|} {|'a|} (xa : eta {|'a|} => (xb : eta {|'a|} => (xc : eta {|'a|} => (xd : eta {|'a|} => B xd) xc) xb) xa)) H x))
A : eta {|prop|type|} => B : eta {|prop|type|} => C : eta {|prop|type|} => {|Pure.equal_intr|axiom|} ({|Pure.imp|const|} A ({|Pure.conjunction|const|} B C)) ({|Pure.conjunction|const|} ({|Pure.imp|const|} A B) ({|Pure.imp|const|} A C)) (H : eps ({|Pure.imp|const|} A ({|Pure.conjunction|const|} B C)) => {|Pure.conjunctionI|thm|} ({|Pure.imp|const|} A B) ({|Pure.imp|const|} A C) (Ha : eps A => {|Pure.conjunctionD1|thm|} B C (H Ha)) (Ha : eps A => {|Pure.conjunctionD2|thm|} B C (H Ha))) (H : eps ({|Pure.conjunction|const|} ({|Pure.imp|const|} A B) ({|Pure.imp|const|} A C)) => Ha : eps A => {|Pure.conjunctionI|thm|} B C ({|Pure.conjunctionD1|thm|} ({|Pure.imp|const|} A B) ({|Pure.imp|const|} A C) H Ha) ({|Pure.conjunctionD2|thm|} ({|Pure.imp|const|} A B) ({|Pure.imp|const|} A C) H Ha))
A : eta {|prop|type|} => B : eta {|prop|type|} => C : eta {|prop|type|} => {|Pure.equal_intr|axiom|} ({|Pure.imp|const|} ({|Pure.conjunction|const|} A B) C) ({|Pure.imp|const|} A ({|Pure.imp|const|} B C)) (H : eps ({|Pure.imp|const|} ({|Pure.conjunction|const|} A B) C) => Ha : eps A => Hb : eps B => H ({|Pure.conjunctionI|thm|} A B Ha Hb)) (H : eps ({|Pure.imp|const|} A ({|Pure.imp|const|} B C)) => Ha : eps ({|Pure.conjunction|const|} A B) => H ({|Pure.conjunctionD1|thm|} A B Ha) ({|Pure.conjunctionD2|thm|} A B Ha))