dedukti-1.0.0: t/Logic.eu
True : Uprop.
I : (eprop True) .
case_0 : (P : Utype -> (f : (etype P) -> (t : (eprop True) -> (_0 : (eprop True) -> (etype P) ) ) ) ) .
I_case_0 : (P : Utype -> (f : (etype P) -> (t : (eprop True) -> (eprop True) ) ) ) .
[P : Utype, f : (etype P) , t : (eprop True) ] ( ( (I_case_0 P) f) t) --> I.
[P : Utype, f : (etype P) , t : (eprop True) ] ( ( ( (case_0 P) f) t) ( ( (I_case_0 P) f) t) ) --> f.
True_rect : (P : Utype -> (f : (etype P) -> (t : (eprop True) -> (etype P) ) ) ) .
[] True_rect --> (P : (etype dottype) => (f : (etype P) => (t : (eprop True) => ( ( ( (case_0 P) f) t) t) ) ) ) .
True_ind : (P : Uprop -> (f : (eprop P) -> (t : (eprop True) -> (eprop P) ) ) ) .
[] True_ind --> (P : (etype dotprop) => (True_rect P) ) .
True_rec : (P : Uset -> (f : (eset P) -> (t : (eprop True) -> (eset P) ) ) ) .
[] True_rec --> (P : (etype dotset) => (True_rect P) ) .
False : Uprop.
case_1 : (P : Utype -> (f : (eprop False) -> (_1 : (eprop False) -> (etype P) ) ) ) .
False_rect : (P : Utype -> (f : (eprop False) -> (etype P) ) ) .
[] False_rect --> (P : (etype dottype) => (f : (eprop False) => ( ( (case_1 P) f) f) ) ) .
False_ind : (P : Uprop -> (f : (eprop False) -> (eprop P) ) ) .
[] False_ind --> (P : (etype dotprop) => (False_rect P) ) .
False_rec : (P : Uset -> (f : (eprop False) -> (eset P) ) ) .
[] False_rec --> (P : (etype dotset) => (False_rect P) ) .
not : (A : Uprop -> Uprop) .
[] not --> (A : (etype dotprop) => ( (dotpipp A) (_2 : (eprop A) => False) ) ) .
and : (A : Uprop -> (B : Uprop -> Uprop) ) .
conj : (A : Uprop -> (B : Uprop -> (_4 : (eprop A) -> (_3 : (eprop B) -> (eprop ( (and A) B) ) ) ) ) ) .
case_2 : (A : Uprop -> (B : Uprop -> (P : Utype -> (f : (_6 : (eprop A) -> (_5 : (eprop B) -> (etype P) ) ) -> (a : (eprop ( (and A) B) ) -> (_7 : (eprop ( (and A) B) ) -> (etype P) ) ) ) ) ) ) .
conj_case_2 : (A : Uprop -> (B : Uprop -> (P : Utype -> (f : (_11 : (eprop A) -> (_10 : (eprop B) -> (etype P) ) ) -> (a : (eprop ( (and A) B) ) -> (_13 : (eprop A) -> (_12 : (eprop B) -> (eprop ( (and A) B) ) ) ) ) ) ) ) ) .
[A : Uprop, B : Uprop, P : Utype, f : (_15 : (eprop A) -> (_14 : (eprop B) -> (etype P) ) ) , a : (eprop ( (and A) B) ) ] ( ( ( ( (conj_case_2 A) B) P) f) a) --> ( (conj A) B) .
[A : Uprop, B : Uprop, P : Utype, f : (_9 : (eprop A) -> (_8 : (eprop B) -> (etype P) ) ) , a : (eprop ( (and A) B) ) , var_0 : (eprop A) , var_1 : (eprop B) ] ( ( ( ( ( (case_2 A) B) P) f) a) ( ( ( ( ( ( (conj_case_2 A) B) P) f) a) var_0) var_1) ) --> ( (f var_0) var_1) .
and_rect : (A : Uprop -> (B : Uprop -> (P : Utype -> (f : (_19 : (eprop A) -> (_18 : (eprop B) -> (etype P) ) ) -> (a : (eprop ( (and A) B) ) -> (etype P) ) ) ) ) ) .
[] and_rect --> (A : (etype dotprop) => (B : (etype dotprop) => (P : (etype dottype) => (f : (etype ( (dotpipt A) (_17 : (eprop A) => ( (dotpipt B) (_16 : (eprop B) => P) ) ) ) ) => (a : (eprop ( (and A) B) ) => ( ( ( ( ( (case_2 A) B) P) f) a) a) ) ) ) ) ) .
and_ind : (A : Uprop -> (B : Uprop -> (P : Uprop -> (f : (_21 : (eprop A) -> (_20 : (eprop B) -> (eprop P) ) ) -> (a : (eprop ( (and A) B) ) -> (eprop P) ) ) ) ) ) .
[] and_ind --> (A : (etype dotprop) => (B : (etype dotprop) => (P : (etype dotprop) => ( ( (and_rect A) B) P) ) ) ) .
and_rec : (A : Uprop -> (B : Uprop -> (P : Uset -> (f : (_23 : (eprop A) -> (_22 : (eprop B) -> (eset P) ) ) -> (a : (eprop ( (and A) B) ) -> (eset P) ) ) ) ) ) .
[] and_rec --> (A : (etype dotprop) => (B : (etype dotprop) => (P : (etype dotset) => ( ( (and_rect A) B) P) ) ) ) .
case_3 : (A : Uprop -> (B : Uprop -> (H : (eprop ( (and A) B) ) -> (_24 : (eprop ( (and A) B) ) -> (eprop A) ) ) ) ) .
conj_case_3 : (A : Uprop -> (B : Uprop -> (H : (eprop ( (and A) B) ) -> (_26 : (eprop A) -> (_25 : (eprop B) -> (eprop ( (and A) B) ) ) ) ) ) ) .
[A : Uprop, B : Uprop, H : (eprop ( (and A) B) ) ] ( ( (conj_case_3 A) B) H) --> ( (conj A) B) .
[A : Uprop, B : Uprop, H : (eprop ( (and A) B) ) , var_2 : (eprop A) , var_3 : (eprop B) ] ( ( ( (case_3 A) B) H) ( ( ( ( (conj_case_3 A) B) H) var_2) var_3) ) --> ( ( (H欧0 : (eprop A) => (H0 : (eprop B) => H欧0) ) var_2) var_3) .
proj1 : (A : Uprop -> (B : Uprop -> (_27 : (eprop ( (and A) B) ) -> (eprop A) ) ) ) .
[] proj1 --> (A : (etype dotprop) => (B : (etype dotprop) => (H : (eprop ( (and A) B) ) => ( ( ( (case_3 A) B) H) H) ) ) ) .
case_4 : (A : Uprop -> (B : Uprop -> (H : (eprop ( (and A) B) ) -> (_28 : (eprop ( (and A) B) ) -> (eprop B) ) ) ) ) .
conj_case_4 : (A : Uprop -> (B : Uprop -> (H : (eprop ( (and A) B) ) -> (_30 : (eprop A) -> (_29 : (eprop B) -> (eprop ( (and A) B) ) ) ) ) ) ) .
[A : Uprop, B : Uprop, H : (eprop ( (and A) B) ) ] ( ( (conj_case_4 A) B) H) --> ( (conj A) B) .
[A : Uprop, B : Uprop, H : (eprop ( (and A) B) ) , var_4 : (eprop A) , var_5 : (eprop B) ] ( ( ( (case_4 A) B) H) ( ( ( ( (conj_case_4 A) B) H) var_4) var_5) ) --> ( ( (H欧0 : (eprop A) => (H0 : (eprop B) => H0) ) var_4) var_5) .
proj2 : (A : Uprop -> (B : Uprop -> (_31 : (eprop ( (and A) B) ) -> (eprop B) ) ) ) .
[] proj2 --> (A : (etype dotprop) => (B : (etype dotprop) => (H : (eprop ( (and A) B) ) => ( ( ( (case_4 A) B) H) H) ) ) ) .
or : (A : Uprop -> (B : Uprop -> Uprop) ) .
or_introl : (A : Uprop -> (B : Uprop -> (_32 : (eprop A) -> (eprop ( (or A) B) ) ) ) ) .
or_intror : (A : Uprop -> (B : Uprop -> (_33 : (eprop B) -> (eprop ( (or A) B) ) ) ) ) .
case_5 : (A : Uprop -> (B : Uprop -> (P : Uprop -> (f : (_34 : (eprop A) -> (eprop P) ) -> (f欧0 : (_35 : (eprop B) -> (eprop P) ) -> (o : (eprop ( (or A) B) ) -> (_36 : (eprop ( (or A) B) ) -> (eprop P) ) ) ) ) ) ) ) .
or_introl_case_5 : (A : Uprop -> (B : Uprop -> (P : Uprop -> (f : (_39 : (eprop A) -> (eprop P) ) -> (f欧0 : (_40 : (eprop B) -> (eprop P) ) -> (o : (eprop ( (or A) B) ) -> (_41 : (eprop A) -> (eprop ( (or A) B) ) ) ) ) ) ) ) ) .
[A : Uprop, B : Uprop, P : Uprop, f : (_42 : (eprop A) -> (eprop P) ) , f欧0 : (_43 : (eprop B) -> (eprop P) ) , o : (eprop ( (or A) B) ) ] ( ( ( ( ( (or_introl_case_5 A) B) P) f) f欧0) o) --> ( (or_introl A) B) .
or_intror_case_5 : (A : Uprop -> (B : Uprop -> (P : Uprop -> (f : (_44 : (eprop A) -> (eprop P) ) -> (f欧0 : (_45 : (eprop B) -> (eprop P) ) -> (o : (eprop ( (or A) B) ) -> (_46 : (eprop B) -> (eprop ( (or A) B) ) ) ) ) ) ) ) ) .
[A : Uprop, B : Uprop, P : Uprop, f : (_47 : (eprop A) -> (eprop P) ) , f欧0 : (_48 : (eprop B) -> (eprop P) ) , o : (eprop ( (or A) B) ) ] ( ( ( ( ( (or_intror_case_5 A) B) P) f) f欧0) o) --> ( (or_intror A) B) .
[A : Uprop, B : Uprop, P : Uprop, f : (_37 : (eprop A) -> (eprop P) ) , f欧0 : (_38 : (eprop B) -> (eprop P) ) , o : (eprop ( (or A) B) ) , var_6 : (eprop A) ] ( ( ( ( ( ( (case_5 A) B) P) f) f欧0) o) ( ( ( ( ( ( (or_introl_case_5 A) B) P) f) f欧0) o) var_6) ) --> (f var_6) .
[A : Uprop, B : Uprop, P : Uprop, f : (_37 : (eprop A) -> (eprop P) ) , f欧0 : (_38 : (eprop B) -> (eprop P) ) , o : (eprop ( (or A) B) ) , var_7 : (eprop B) ] ( ( ( ( ( ( (case_5 A) B) P) f) f欧0) o) ( ( ( ( ( ( (or_intror_case_5 A) B) P) f) f欧0) o) var_7) ) --> (f欧0 var_7) .
or_ind : (A : Uprop -> (B : Uprop -> (P : Uprop -> (f : (_51 : (eprop A) -> (eprop P) ) -> (f欧0 : (_52 : (eprop B) -> (eprop P) ) -> (o : (eprop ( (or A) B) ) -> (eprop P) ) ) ) ) ) ) .
[] or_ind --> (A : (etype dotprop) => (B : (etype dotprop) => (P : (etype dotprop) => (f : (eprop ( (dotpipp A) (_50 : (eprop A) => P) ) ) => (f欧0 : (eprop ( (dotpipp B) (_49 : (eprop B) => P) ) ) => (o : (eprop ( (or A) B) ) => ( ( ( ( ( ( (case_5 A) B) P) f) f欧0) o) o) ) ) ) ) ) ) .
iff : (A : Uprop -> (B : Uprop -> Uprop) ) .
[] iff --> (A : (etype dotprop) => (B : (etype dotprop) => ( (and ( (dotpipp A) (_53 : (eprop A) => B) ) ) ( (dotpipp B) (_54 : (eprop B) => A) ) ) ) ) .
iff_refl : (A : Uprop -> (eprop ( (iff A) A) ) ) .
[] iff_refl --> (A : (etype dotprop) => ( ( ( (conj ( (dotpipp A) (_55 : (eprop A) => A) ) ) ( (dotpipp A) (_56 : (eprop A) => A) ) ) (H : (eprop A) => H) ) (H : (eprop A) => H) ) ) .
case_6 : (A : Uprop -> (B : Uprop -> (C : Uprop -> (H : (eprop ( (iff A) B) ) -> (_60 : (eprop ( (and ( (dotpipp A) (_57 : (eprop A) => B) ) ) ( (dotpipp B) (_58 : (eprop B) => A) ) ) ) -> (_59 : (eprop ( (iff B) C) ) -> (eprop ( (iff A) C) ) ) ) ) ) ) ) .
conj_case_6 : (A : Uprop -> (B : Uprop -> (C : Uprop -> (H : (eprop ( (iff A) B) ) -> (_68 : (_63 : (eprop A) -> (eprop B) ) -> (_67 : (_64 : (eprop B) -> (eprop A) ) -> (eprop ( (and ( (dotpipp A) (_65 : (eprop A) => B) ) ) ( (dotpipp B) (_66 : (eprop B) => A) ) ) ) ) ) ) ) ) ) .
[A : Uprop, B : Uprop, C : Uprop, H : (eprop ( (iff A) B) ) ] ( ( ( (conj_case_6 A) B) C) H) --> ( (conj ( (dotpipp A) (_61 : (eprop A) => B) ) ) ( (dotpipp B) (_62 : (eprop B) => A) ) ) .
case_7 : (A : Uprop -> (B : Uprop -> (C : Uprop -> (H : (eprop ( (iff A) B) ) -> (H1 : (_71 : (eprop A) -> (eprop B) ) -> (H2 : (_72 : (eprop B) -> (eprop A) ) -> (H欧0 : (eprop ( (iff B) C) ) -> (_75 : (eprop ( (and ( (dotpipp B) (_73 : (eprop B) => C) ) ) ( (dotpipp C) (_74 : (eprop C) => B) ) ) ) -> (eprop ( (iff A) C) ) ) ) ) ) ) ) ) ) .
conj_case_7 : (A : Uprop -> (B : Uprop -> (C : Uprop -> (H : (eprop ( (iff A) B) ) -> (H1 : (_80 : (eprop A) -> (eprop B) ) -> (H2 : (_81 : (eprop B) -> (eprop A) ) -> (H欧0 : (eprop ( (iff B) C) ) -> (_87 : (_82 : (eprop B) -> (eprop C) ) -> (_86 : (_83 : (eprop C) -> (eprop B) ) -> (eprop ( (and ( (dotpipp B) (_84 : (eprop B) => C) ) ) ( (dotpipp C) (_85 : (eprop C) => B) ) ) ) ) ) ) ) ) ) ) ) ) .
[A : Uprop, B : Uprop, C : Uprop, H : (eprop ( (iff A) B) ) , H1 : (_88 : (eprop A) -> (eprop B) ) , H2 : (_89 : (eprop B) -> (eprop A) ) , H欧0 : (eprop ( (iff B) C) ) ] ( ( ( ( ( ( (conj_case_7 A) B) C) H) H1) H2) H欧0) --> ( (conj ( (dotpipp B) (_78 : (eprop B) => C) ) ) ( (dotpipp C) (_79 : (eprop C) => B) ) ) .
[A : Uprop, B : Uprop, C : Uprop, H : (eprop ( (iff A) B) ) , H1 : (_76 : (eprop A) -> (eprop B) ) , H2 : (_77 : (eprop B) -> (eprop A) ) , H欧0 : (eprop ( (iff B) C) ) , var_10 : (_90 : (eprop B) -> (eprop C) ) , var_11 : (_91 : (eprop C) -> (eprop B) ) ] ( ( ( ( ( ( ( (case_7 A) B) C) H) H1) H2) H欧0) ( ( ( ( ( ( ( ( (conj_case_7 A) B) C) H) H1) H2) H欧0) var_10) var_11) ) --> ( ( (H3 : (eprop ( (dotpipp B) (_95 : (eprop B) => C) ) ) => (H4 : (eprop ( (dotpipp C) (_94 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp A) (_92 : (eprop A) => C) ) ) ( (dotpipp C) (_93 : (eprop C) => A) ) ) (H欧1 : (eprop A) => (H3 (H1 H欧1) ) ) ) (H欧1 : (eprop C) => (H2 (H1 (H2 (H4 H欧1) ) ) ) ) ) ) ) var_10) var_11) .
[A : Uprop, B : Uprop, C : Uprop, H : (eprop ( (iff A) B) ) , var_8 : (_69 : (eprop A) -> (eprop B) ) , var_9 : (_70 : (eprop B) -> (eprop A) ) ] ( ( ( ( (case_6 A) B) C) H) ( ( ( ( ( (conj_case_6 A) B) C) H) var_8) var_9) ) --> ( ( (H1 : (eprop ( (dotpipp A) (_97 : (eprop A) => B) ) ) => (H2 : (eprop ( (dotpipp B) (_96 : (eprop B) => A) ) ) => (H欧0 : (eprop ( (iff B) C) ) => ( ( ( ( ( ( ( (case_7 A) B) C) H) H1) H2) H欧0) H欧0) ) ) ) var_8) var_9) .
iff_trans : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_99 : (eprop ( (iff A) B) ) -> (_98 : (eprop ( (iff B) C) ) -> (eprop ( (iff A) C) ) ) ) ) ) ) .
[] iff_trans --> (A : (etype dotprop) => (B : (etype dotprop) => (C : (etype dotprop) => (H : (eprop ( (iff A) B) ) => ( ( ( ( (case_6 A) B) C) H) H) ) ) ) ) .
case_8 : (A : Uprop -> (B : Uprop -> (H : (eprop ( (iff A) B) ) -> (_102 : (eprop ( (and ( (dotpipp A) (_100 : (eprop A) => B) ) ) ( (dotpipp B) (_101 : (eprop B) => A) ) ) ) -> (eprop ( (iff B) A) ) ) ) ) ) .
conj_case_8 : (A : Uprop -> (B : Uprop -> (H : (eprop ( (iff A) B) ) -> (_110 : (_105 : (eprop A) -> (eprop B) ) -> (_109 : (_106 : (eprop B) -> (eprop A) ) -> (eprop ( (and ( (dotpipp A) (_107 : (eprop A) => B) ) ) ( (dotpipp B) (_108 : (eprop B) => A) ) ) ) ) ) ) ) ) .
[A : Uprop, B : Uprop, H : (eprop ( (iff A) B) ) ] ( ( (conj_case_8 A) B) H) --> ( (conj ( (dotpipp A) (_103 : (eprop A) => B) ) ) ( (dotpipp B) (_104 : (eprop B) => A) ) ) .
[A : Uprop, B : Uprop, H : (eprop ( (iff A) B) ) , var_12 : (_111 : (eprop A) -> (eprop B) ) , var_13 : (_112 : (eprop B) -> (eprop A) ) ] ( ( ( (case_8 A) B) H) ( ( ( ( (conj_case_8 A) B) H) var_12) var_13) ) --> ( ( (H1 : (eprop ( (dotpipp A) (_116 : (eprop A) => B) ) ) => (H2 : (eprop ( (dotpipp B) (_115 : (eprop B) => A) ) ) => ( ( ( (conj ( (dotpipp B) (_113 : (eprop B) => A) ) ) ( (dotpipp A) (_114 : (eprop A) => B) ) ) H2) H1) ) ) var_12) var_13) .
iff_sym : (A : Uprop -> (B : Uprop -> (_117 : (eprop ( (iff A) B) ) -> (eprop ( (iff B) A) ) ) ) ) .
[] iff_sym --> (A : (etype dotprop) => (B : (etype dotprop) => (H : (eprop ( (iff A) B) ) => ( ( ( (case_8 A) B) H) H) ) ) ) .
case_9 : (A : Uprop -> (H : (eprop ( (iff A) False) ) -> (_128 : (eprop ( (and ( (dotpipp A) (_125 : (eprop A) => False) ) ) ( (dotpipp False) (_126 : (eprop False) => A) ) ) ) -> (_127 : (eprop A) -> (eprop False) ) ) ) ) .
conj_case_9 : (A : Uprop -> (H : (eprop ( (iff A) False) ) -> (_136 : (_131 : (eprop A) -> (eprop False) ) -> (_135 : (_132 : (eprop False) -> (eprop A) ) -> (eprop ( (and ( (dotpipp A) (_133 : (eprop A) => False) ) ) ( (dotpipp False) (_134 : (eprop False) => A) ) ) ) ) ) ) ) .
[A : Uprop, H : (eprop ( (iff A) False) ) ] ( (conj_case_9 A) H) --> ( (conj ( (dotpipp A) (_129 : (eprop A) => False) ) ) ( (dotpipp False) (_130 : (eprop False) => A) ) ) .
[A : Uprop, H : (eprop ( (iff A) False) ) , var_14 : (_137 : (eprop A) -> (eprop False) ) , var_15 : (_138 : (eprop False) -> (eprop A) ) ] ( ( (case_9 A) H) ( ( ( (conj_case_9 A) H) var_14) var_15) ) --> ( ( (H欧0 : (eprop ( (dotpipp A) (_140 : (eprop A) => False) ) ) => (H0 : (eprop ( (dotpipp False) (_139 : (eprop False) => A) ) ) => H欧0) ) var_14) var_15) .
neg_false : (A : Uprop -> (eprop ( (iff (not A) ) ( (iff A) False) ) ) ) .
[] neg_false --> (A : (etype dotprop) => ( ( ( (conj ( (dotpipp ( (dotpipp A) (_118 : (eprop A) => False) ) ) (_119 : (eprop ( (dotpipp A) (_118 : (eprop A) => False) ) ) => ( (iff A) False) ) ) ) ( (dotpipp ( (iff A) False) ) (_121 : (eprop ( (iff A) False) ) => ( (dotpipp A) (_120 : (eprop A) => False) ) ) ) ) (H : (eprop ( (dotpipp A) (_124 : (eprop A) => False) ) ) => ( ( ( (conj ( (dotpipp A) (_122 : (eprop A) => False) ) ) ( (dotpipp False) (_123 : (eprop False) => A) ) ) H) (H1 : (eprop False) => ( (False_ind A) H1) ) ) ) ) (H : (eprop ( (iff A) False) ) => ( ( (case_9 A) H) H) ) ) ) .
and_cancel_l : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_168 : (_165 : (eprop B) -> (eprop A) ) -> (_167 : (_166 : (eprop C) -> (eprop A) ) -> (eprop ( (iff ( (iff ( (and A) B) ) ( (and A) C) ) ) ( (iff B) C) ) ) ) ) ) ) ) .
[] and_cancel_l --> (A : (etype dotprop) => (B : (etype dotprop) => (C : (etype dotprop) => (H : (eprop ( (dotpipp B) (_164 : (eprop B) => A) ) ) => (H0 : (eprop ( (dotpipp C) (_163 : (eprop C) => A) ) ) => ( ( ( (conj ( (dotpipp ( (iff ( (and A) B) ) ( (and A) C) ) ) (_141 : (eprop ( (iff ( (and A) B) ) ( (and A) C) ) ) => ( (iff B) C) ) ) ) ( (dotpipp ( (iff B) C) ) (_142 : (eprop ( (iff B) C) ) => ( (iff ( (and A) B) ) ( (and A) C) ) ) ) ) (H1 : (eprop ( (iff ( (and A) B) ) ( (and A) C) ) ) => ( ( ( ( (and_ind ( (dotpipp ( (and A) B) ) (_143 : (eprop ( (and A) B) ) => ( (and A) C) ) ) ) ( (dotpipp ( (and A) C) ) (_144 : (eprop ( (and A) C) ) => ( (and A) B) ) ) ) ( (iff B) C) ) (H2 : (eprop ( (dotpipp ( (and A) B) ) (_156 : (eprop ( (and A) B) ) => ( (and A) C) ) ) ) => (H3 : (eprop ( (dotpipp ( (and A) C) ) (_155 : (eprop ( (and A) C) ) => ( (and A) B) ) ) ) => ( (H1欧0 : (eprop ( (dotpipp A) (_154 : (eprop A) => ( (dotpipp B) (_153 : (eprop B) => ( (and A) C) ) ) ) ) ) => ( (H2欧0 : (eprop ( (dotpipp A) (_152 : (eprop A) => ( (dotpipp C) (_151 : (eprop C) => ( (and A) B) ) ) ) ) ) => ( ( ( (conj ( (dotpipp B) (_145 : (eprop B) => C) ) ) ( (dotpipp C) (_146 : (eprop C) => B) ) ) (H3欧0 : (eprop B) => ( (H4 : (eprop A) => ( (H欧0 : (eprop ( (dotpipp B) (_148 : (eprop B) => ( (and A) C) ) ) ) => ( (H1欧1 : (eprop ( (and A) C) ) => ( ( ( ( (and_ind A) C) C) (H欧1 : (eprop A) => (H5 : (eprop C) => ( (H1欧2 : (eprop ( (dotpipp C) (_147 : (eprop C) => ( (and A) B) ) ) ) => ( (H2欧1 : (eprop A) => ( (H0欧0 : (eprop ( (and A) B) ) => ( ( ( ( (and_ind A) B) C) (H1欧3 : (eprop A) => (H6 : (eprop B) => H5) ) ) H0欧0) ) (H1欧2 H5) ) ) (H0 H5) ) ) (H2欧0 H4) ) ) ) ) H1欧1) ) (H欧0 H3欧0) ) ) (H1欧0 H4) ) ) (H H3欧0) ) ) ) (H3欧0 : (eprop C) => ( (H4 : (eprop A) => ( (H0欧0 : (eprop ( (dotpipp B) (_150 : (eprop B) => ( (and A) C) ) ) ) => ( (H1欧1 : (eprop ( (dotpipp C) (_149 : (eprop C) => ( (and A) B) ) ) ) => ( (H2欧1 : (eprop ( (and A) B) ) => ( ( ( ( (and_ind A) B) B) (H1欧2 : (eprop A) => (H5 : (eprop B) => ( (H2欧2 : (eprop A) => ( (H欧0 : (eprop ( (and A) C) ) => ( ( ( ( (and_ind A) C) B) (H0欧1 : (eprop A) => (H6 : (eprop C) => H5) ) ) H欧0) ) (H0欧0 H5) ) ) (H H5) ) ) ) ) H2欧1) ) (H1欧1 H3欧0) ) ) (H2欧0 H4) ) ) (H1欧0 H4) ) ) (H0 H3欧0) ) ) ) ) (H2欧0 : (eprop A) => (H4 : (eprop C) => (H3 ( ( ( (conj A) C) H2欧0) H4) ) ) ) ) ) (H1欧0 : (eprop A) => (H4 : (eprop B) => (H2 ( ( ( (conj A) B) H1欧0) H4) ) ) ) ) ) ) ) H1) ) ) (H1 : (eprop ( (iff B) C) ) => ( ( ( ( (and_ind ( (dotpipp B) (_157 : (eprop B) => C) ) ) ( (dotpipp C) (_158 : (eprop C) => B) ) ) ( (iff ( (and A) B) ) ( (and A) C) ) ) (H2 : (eprop ( (dotpipp B) (_162 : (eprop B) => C) ) ) => (H3 : (eprop ( (dotpipp C) (_161 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (and A) B) ) (_159 : (eprop ( (and A) B) ) => ( (and A) C) ) ) ) ( (dotpipp ( (and A) C) ) (_160 : (eprop ( (and A) C) ) => ( (and A) B) ) ) ) (H1欧0 : (eprop ( (and A) B) ) => ( ( ( ( (and_ind A) B) ( (and A) C) ) (H4 : (eprop A) => (H5 : (eprop B) => ( (H1欧1 : (eprop A) => ( (H欧0 : (eprop C) => ( (H2欧0 : (eprop A) => ( (H0欧0 : (eprop B) => ( ( ( (conj A) C) H2欧0) H欧0) ) (H3 H欧0) ) ) (H0 H欧0) ) ) (H2 H5) ) ) (H H5) ) ) ) ) H1欧0) ) ) (H1欧0 : (eprop ( (and A) C) ) => ( ( ( ( (and_ind A) C) ( (and A) B) ) (H4 : (eprop A) => (H5 : (eprop C) => ( (H1欧1 : (eprop A) => ( (H0欧0 : (eprop B) => ( (H3欧0 : (eprop A) => ( (H欧0 : (eprop C) => ( ( ( (conj A) B) H3欧0) H0欧0) ) (H2 H0欧0) ) ) (H H0欧0) ) ) (H3 H5) ) ) (H0 H5) ) ) ) ) H1欧0) ) ) ) ) ) H1) ) ) ) ) ) ) ) .
and_cancel_r : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_196 : (_193 : (eprop B) -> (eprop A) ) -> (_195 : (_194 : (eprop C) -> (eprop A) ) -> (eprop ( (iff ( (iff ( (and B) A) ) ( (and C) A) ) ) ( (iff B) C) ) ) ) ) ) ) ) .
[] and_cancel_r --> (A : (etype dotprop) => (B : (etype dotprop) => (C : (etype dotprop) => (H : (eprop ( (dotpipp B) (_192 : (eprop B) => A) ) ) => (H0 : (eprop ( (dotpipp C) (_191 : (eprop C) => A) ) ) => ( ( ( (conj ( (dotpipp ( (iff ( (and B) A) ) ( (and C) A) ) ) (_169 : (eprop ( (iff ( (and B) A) ) ( (and C) A) ) ) => ( (iff B) C) ) ) ) ( (dotpipp ( (iff B) C) ) (_170 : (eprop ( (iff B) C) ) => ( (iff ( (and B) A) ) ( (and C) A) ) ) ) ) (H1 : (eprop ( (iff ( (and B) A) ) ( (and C) A) ) ) => ( ( ( ( (and_ind ( (dotpipp ( (and B) A) ) (_171 : (eprop ( (and B) A) ) => ( (and C) A) ) ) ) ( (dotpipp ( (and C) A) ) (_172 : (eprop ( (and C) A) ) => ( (and B) A) ) ) ) ( (iff B) C) ) (H2 : (eprop ( (dotpipp ( (and B) A) ) (_184 : (eprop ( (and B) A) ) => ( (and C) A) ) ) ) => (H3 : (eprop ( (dotpipp ( (and C) A) ) (_183 : (eprop ( (and C) A) ) => ( (and B) A) ) ) ) => ( (H1欧0 : (eprop ( (dotpipp B) (_182 : (eprop B) => ( (dotpipp A) (_181 : (eprop A) => ( (and C) A) ) ) ) ) ) => ( (H2欧0 : (eprop ( (dotpipp C) (_180 : (eprop C) => ( (dotpipp A) (_179 : (eprop A) => ( (and B) A) ) ) ) ) ) => ( ( ( (conj ( (dotpipp B) (_173 : (eprop B) => C) ) ) ( (dotpipp C) (_174 : (eprop C) => B) ) ) (H3欧0 : (eprop B) => ( (H4 : (eprop A) => ( (H欧0 : (eprop ( (dotpipp A) (_176 : (eprop A) => ( (and C) A) ) ) ) => ( (H1欧1 : (eprop ( (and C) A) ) => ( ( ( ( (and_ind C) A) C) (H欧1 : (eprop C) => (H5 : (eprop A) => ( (H1欧2 : (eprop A) => ( (H0欧0 : (eprop ( (dotpipp A) (_175 : (eprop A) => ( (and B) A) ) ) ) => ( (H2欧1 : (eprop ( (and B) A) ) => ( ( ( ( (and_ind B) A) C) (H0欧1 : (eprop B) => (H6 : (eprop A) => H欧1) ) ) H2欧1) ) (H0欧0 H4) ) ) (H2欧0 H欧1) ) ) (H0 H欧1) ) ) ) ) H1欧1) ) (H欧0 H4) ) ) (H1欧0 H3欧0) ) ) (H H3欧0) ) ) ) (H3欧0 : (eprop C) => ( (H4 : (eprop A) => ( (H0欧0 : (eprop ( (dotpipp A) (_178 : (eprop A) => ( (and B) A) ) ) ) => ( (H2欧1 : (eprop ( (and B) A) ) => ( ( ( ( (and_ind B) A) B) (H0欧1 : (eprop B) => (H5 : (eprop A) => ( (H2欧2 : (eprop A) => ( (H欧0 : (eprop ( (dotpipp A) (_177 : (eprop A) => ( (and C) A) ) ) ) => ( (H1欧1 : (eprop ( (and C) A) ) => ( ( ( ( (and_ind C) A) B) (H欧1 : (eprop C) => (H6 : (eprop A) => H0欧1) ) ) H1欧1) ) (H欧0 H4) ) ) (H1欧0 H0欧1) ) ) (H H0欧1) ) ) ) ) H2欧1) ) (H0欧0 H4) ) ) (H2欧0 H3欧0) ) ) (H0 H3欧0) ) ) ) ) (H2欧0 : (eprop C) => (H4 : (eprop A) => (H3 ( ( ( (conj C) A) H2欧0) H4) ) ) ) ) ) (H1欧0 : (eprop B) => (H4 : (eprop A) => (H2 ( ( ( (conj B) A) H1欧0) H4) ) ) ) ) ) ) ) H1) ) ) (H1 : (eprop ( (iff B) C) ) => ( ( ( ( (and_ind ( (dotpipp B) (_185 : (eprop B) => C) ) ) ( (dotpipp C) (_186 : (eprop C) => B) ) ) ( (iff ( (and B) A) ) ( (and C) A) ) ) (H2 : (eprop ( (dotpipp B) (_190 : (eprop B) => C) ) ) => (H3 : (eprop ( (dotpipp C) (_189 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (and B) A) ) (_187 : (eprop ( (and B) A) ) => ( (and C) A) ) ) ) ( (dotpipp ( (and C) A) ) (_188 : (eprop ( (and C) A) ) => ( (and B) A) ) ) ) (H1欧0 : (eprop ( (and B) A) ) => ( ( ( ( (and_ind B) A) ( (and C) A) ) (H4 : (eprop B) => (H5 : (eprop A) => ( (H1欧1 : (eprop A) => ( (H欧0 : (eprop C) => ( (H2欧0 : (eprop A) => ( (H0欧0 : (eprop B) => ( ( ( (conj C) A) H欧0) H2欧0) ) (H3 H欧0) ) ) (H0 H欧0) ) ) (H2 H4) ) ) (H H4) ) ) ) ) H1欧0) ) ) (H1欧0 : (eprop ( (and C) A) ) => ( ( ( ( (and_ind C) A) ( (and B) A) ) (H4 : (eprop C) => (H5 : (eprop A) => ( (H1欧1 : (eprop A) => ( (H0欧0 : (eprop B) => ( (H3欧0 : (eprop A) => ( (H欧0 : (eprop C) => ( ( ( (conj B) A) H0欧0) H3欧0) ) (H2 H0欧0) ) ) (H H0欧0) ) ) (H3 H4) ) ) (H0 H4) ) ) ) ) H1欧0) ) ) ) ) ) H1) ) ) ) ) ) ) ) .
or_cancel_l : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_220 : (_217 : (eprop B) -> (eprop (not A) ) ) -> (_219 : (_218 : (eprop C) -> (eprop (not A) ) ) -> (eprop ( (iff ( (iff ( (or A) B) ) ( (or A) C) ) ) ( (iff B) C) ) ) ) ) ) ) ) .
[] or_cancel_l --> (A : (etype dotprop) => (B : (etype dotprop) => (C : (etype dotprop) => (H : (eprop ( (dotpipp B) (_216 : (eprop B) => (not A) ) ) ) => (H0 : (eprop ( (dotpipp C) (_215 : (eprop C) => (not A) ) ) ) => ( ( ( (conj ( (dotpipp ( (iff ( (or A) B) ) ( (or A) C) ) ) (_197 : (eprop ( (iff ( (or A) B) ) ( (or A) C) ) ) => ( (iff B) C) ) ) ) ( (dotpipp ( (iff B) C) ) (_198 : (eprop ( (iff B) C) ) => ( (iff ( (or A) B) ) ( (or A) C) ) ) ) ) (H1 : (eprop ( (iff ( (or A) B) ) ( (or A) C) ) ) => ( ( ( ( (and_ind ( (dotpipp ( (or A) B) ) (_199 : (eprop ( (or A) B) ) => ( (or A) C) ) ) ) ( (dotpipp ( (or A) C) ) (_200 : (eprop ( (or A) C) ) => ( (or A) B) ) ) ) ( (iff B) C) ) (H2 : (eprop ( (dotpipp ( (or A) B) ) (_208 : (eprop ( (or A) B) ) => ( (or A) C) ) ) ) => (H3 : (eprop ( (dotpipp ( (or A) C) ) (_207 : (eprop ( (or A) C) ) => ( (or A) B) ) ) ) => ( (H1欧0 : (eprop ( (dotpipp A) (_206 : (eprop A) => ( (or A) C) ) ) ) => ( (H4 : (eprop ( (dotpipp B) (_205 : (eprop B) => ( (or A) C) ) ) ) => ( (H2欧0 : (eprop ( (dotpipp A) (_204 : (eprop A) => ( (or A) B) ) ) ) => ( (H5 : (eprop ( (dotpipp C) (_203 : (eprop C) => ( (or A) B) ) ) ) => ( ( ( (conj ( (dotpipp B) (_201 : (eprop B) => C) ) ) ( (dotpipp C) (_202 : (eprop C) => B) ) ) (H3欧0 : (eprop B) => ( (H6 : (eprop (not A) ) => ( (H欧0 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) C) (H4欧0 : (eprop A) => ( (H欧1 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) C) (H1欧1 : (eprop A) => ( (H欧2 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H2欧1 : (eprop A) => ( (H欧3 : (eprop False) => ( (False_ind C) H欧3) ) (H6 H4欧0) ) ) ) (H2欧1 : (eprop B) => ( (H欧3 : (eprop False) => ( (False_ind C) H欧3) ) (H6 H4欧0) ) ) ) H欧2) ) (H2欧0 H4欧0) ) ) ) (H1欧1 : (eprop C) => ( (H欧2 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H2欧1 : (eprop A) => ( (H欧3 : (eprop False) => ( (H6欧0 : (eprop (not A) ) => ( (H0欧0 : (eprop False) => ( (H6欧1 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H5欧0 : (eprop A) => ( (False_ind C) H0欧0) ) ) (H5欧0 : (eprop B) => ( (False_ind C) H0欧0) ) ) H6欧1) ) (H5 H1欧1) ) ) (H6欧0 H4欧0) ) ) (H0 H1欧1) ) ) (H6 H4欧0) ) ) ) (H2欧1 : (eprop B) => ( (H欧3 : (eprop False) => ( (H6欧0 : (eprop (not A) ) => ( (H0欧0 : (eprop False) => ( (H6欧1 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H5欧0 : (eprop A) => ( (False_ind C) H0欧0) ) ) (H5欧0 : (eprop B) => ( (False_ind C) H0欧0) ) ) H6欧1) ) (H5 H1欧1) ) ) (H6欧0 H4欧0) ) ) (H0 H1欧1) ) ) (H6 H4欧0) ) ) ) H欧2) ) (H2欧0 H4欧0) ) ) ) H欧1) ) (H1欧0 H4欧0) ) ) ) (H4欧0 : (eprop C) => ( (H欧1 : (eprop (not A) ) => ( (H0欧0 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H5欧0 : (eprop A) => ( (H0欧1 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) C) (H1欧1 : (eprop A) => ( (H0欧2 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H2欧1 : (eprop A) => ( (H0欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind C) H6欧0) ) (H欧1 H5欧0) ) ) (H6 H5欧0) ) ) ) (H2欧1 : (eprop B) => ( (H0欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind C) H6欧0) ) (H欧1 H5欧0) ) ) (H6 H5欧0) ) ) ) H0欧2) ) (H2欧0 H5欧0) ) ) ) (H1欧1 : (eprop C) => ( (H0欧2 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H2欧1 : (eprop A) => ( (H0欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind C) H6欧0) ) (H欧1 H5欧0) ) ) (H6 H5欧0) ) ) ) (H2欧1 : (eprop B) => ( (H0欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind C) H6欧0) ) (H欧1 H5欧0) ) ) (H6 H5欧0) ) ) ) H0欧2) ) (H2欧0 H5欧0) ) ) ) H0欧1) ) (H1欧0 H5欧0) ) ) ) (H5欧0 : (eprop B) => H4欧0) ) H0欧0) ) (H5 H4欧0) ) ) (H0 H4欧0) ) ) ) H欧0) ) (H4 H3欧0) ) ) (H H3欧0) ) ) ) (H3欧0 : (eprop C) => ( (H6 : (eprop (not A) ) => ( (H0欧0 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) B) (H5欧0 : (eprop A) => ( (H0欧1 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) B) (H1欧1 : (eprop A) => ( (H0欧2 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) B) (H2欧1 : (eprop A) => ( (H0欧3 : (eprop False) => ( (False_ind B) H0欧3) ) (H6 H5欧0) ) ) ) (H2欧1 : (eprop B) => ( (H0欧3 : (eprop False) => ( (H6欧0 : (eprop (not A) ) => ( (H欧0 : (eprop False) => ( (H6欧1 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) B) (H4欧0 : (eprop A) => ( (False_ind B) H欧0) ) ) (H4欧0 : (eprop C) => ( (False_ind B) H欧0) ) ) H6欧1) ) (H4 H2欧1) ) ) (H6欧0 H5欧0) ) ) (H H2欧1) ) ) (H6 H5欧0) ) ) ) H0欧2) ) (H2欧0 H5欧0) ) ) ) (H1欧1 : (eprop C) => ( (H0欧2 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) B) (H2欧1 : (eprop A) => ( (H0欧3 : (eprop False) => ( (False_ind B) H0欧3) ) (H6 H5欧0) ) ) ) (H2欧1 : (eprop B) => ( (H0欧3 : (eprop False) => ( (H6欧0 : (eprop (not A) ) => ( (H欧0 : (eprop False) => ( (H6欧1 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) B) (H4欧0 : (eprop A) => ( (False_ind B) H欧0) ) ) (H4欧0 : (eprop C) => ( (False_ind B) H欧0) ) ) H6欧1) ) (H4 H2欧1) ) ) (H6欧0 H5欧0) ) ) (H H2欧1) ) ) (H6 H5欧0) ) ) ) H0欧2) ) (H2欧0 H5欧0) ) ) ) H0欧1) ) (H1欧0 H5欧0) ) ) ) (H5欧0 : (eprop B) => ( (H0欧1 : (eprop (not A) ) => ( (H欧0 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) B) (H4欧0 : (eprop A) => ( (H欧1 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) B) (H1欧1 : (eprop A) => ( (H欧2 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) B) (H2欧1 : (eprop A) => ( (H欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind B) H6欧0) ) (H0欧1 H4欧0) ) ) (H6 H4欧0) ) ) ) (H2欧1 : (eprop B) => ( (H欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind B) H6欧0) ) (H0欧1 H4欧0) ) ) (H6 H4欧0) ) ) ) H欧2) ) (H2欧0 H4欧0) ) ) ) (H1欧1 : (eprop C) => ( (H欧2 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) B) (H2欧1 : (eprop A) => ( (H欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind B) H6欧0) ) (H0欧1 H4欧0) ) ) (H6 H4欧0) ) ) ) (H2欧1 : (eprop B) => ( (H欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind B) H6欧0) ) (H0欧1 H4欧0) ) ) (H6 H4欧0) ) ) ) H欧2) ) (H2欧0 H4欧0) ) ) ) H欧1) ) (H1欧0 H4欧0) ) ) ) (H4欧0 : (eprop C) => H5欧0) ) H欧0) ) (H4 H5欧0) ) ) (H H5欧0) ) ) ) H0欧0) ) (H5 H3欧0) ) ) (H0 H3欧0) ) ) ) ) (H5 : (eprop C) => (H3 ( ( (or_intror A) C) H5) ) ) ) ) (H2欧0 : (eprop A) => (H3 ( ( (or_introl A) C) H2欧0) ) ) ) ) (H4 : (eprop B) => (H2 ( ( (or_intror A) B) H4) ) ) ) ) (H1欧0 : (eprop A) => (H2 ( ( (or_introl A) B) H1欧0) ) ) ) ) ) ) H1) ) ) (H1 : (eprop ( (iff B) C) ) => ( ( ( ( (and_ind ( (dotpipp B) (_209 : (eprop B) => C) ) ) ( (dotpipp C) (_210 : (eprop C) => B) ) ) ( (iff ( (or A) B) ) ( (or A) C) ) ) (H2 : (eprop ( (dotpipp B) (_214 : (eprop B) => C) ) ) => (H3 : (eprop ( (dotpipp C) (_213 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (or A) B) ) (_211 : (eprop ( (or A) B) ) => ( (or A) C) ) ) ) ( (dotpipp ( (or A) C) ) (_212 : (eprop ( (or A) C) ) => ( (or A) B) ) ) ) (H1欧0 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) ( (or A) C) ) (H4 : (eprop A) => ( ( (or_introl A) C) H4) ) ) (H4 : (eprop B) => ( (H1欧1 : (eprop (not A) ) => ( (H欧0 : (eprop C) => ( (H2欧0 : (eprop (not A) ) => ( (H0欧0 : (eprop B) => ( ( (or_intror A) C) H欧0) ) (H3 H欧0) ) ) (H0 H欧0) ) ) (H2 H4) ) ) (H H4) ) ) ) H1欧0) ) ) (H1欧0 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) ( (or A) B) ) (H4 : (eprop A) => ( ( (or_introl A) B) H4) ) ) (H4 : (eprop C) => ( (H1欧1 : (eprop (not A) ) => ( (H0欧0 : (eprop B) => ( (H3欧0 : (eprop (not A) ) => ( (H欧0 : (eprop C) => ( ( (or_intror A) B) H0欧0) ) (H2 H0欧0) ) ) (H H0欧0) ) ) (H3 H4) ) ) (H0 H4) ) ) ) H1欧0) ) ) ) ) ) H1) ) ) ) ) ) ) ) .
or_cancel_r : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_244 : (_241 : (eprop B) -> (eprop (not A) ) ) -> (_243 : (_242 : (eprop C) -> (eprop (not A) ) ) -> (eprop ( (iff ( (iff ( (or B) A) ) ( (or C) A) ) ) ( (iff B) C) ) ) ) ) ) ) ) .
[] or_cancel_r --> (A : (etype dotprop) => (B : (etype dotprop) => (C : (etype dotprop) => (H : (eprop ( (dotpipp B) (_240 : (eprop B) => (not A) ) ) ) => (H0 : (eprop ( (dotpipp C) (_239 : (eprop C) => (not A) ) ) ) => ( ( ( (conj ( (dotpipp ( (iff ( (or B) A) ) ( (or C) A) ) ) (_221 : (eprop ( (iff ( (or B) A) ) ( (or C) A) ) ) => ( (iff B) C) ) ) ) ( (dotpipp ( (iff B) C) ) (_222 : (eprop ( (iff B) C) ) => ( (iff ( (or B) A) ) ( (or C) A) ) ) ) ) (H1 : (eprop ( (iff ( (or B) A) ) ( (or C) A) ) ) => ( ( ( ( (and_ind ( (dotpipp ( (or B) A) ) (_223 : (eprop ( (or B) A) ) => ( (or C) A) ) ) ) ( (dotpipp ( (or C) A) ) (_224 : (eprop ( (or C) A) ) => ( (or B) A) ) ) ) ( (iff B) C) ) (H2 : (eprop ( (dotpipp ( (or B) A) ) (_232 : (eprop ( (or B) A) ) => ( (or C) A) ) ) ) => (H3 : (eprop ( (dotpipp ( (or C) A) ) (_231 : (eprop ( (or C) A) ) => ( (or B) A) ) ) ) => ( (H1欧0 : (eprop ( (dotpipp B) (_230 : (eprop B) => ( (or C) A) ) ) ) => ( (H4 : (eprop ( (dotpipp A) (_229 : (eprop A) => ( (or C) A) ) ) ) => ( (H2欧0 : (eprop ( (dotpipp C) (_228 : (eprop C) => ( (or B) A) ) ) ) => ( (H5 : (eprop ( (dotpipp A) (_227 : (eprop A) => ( (or B) A) ) ) ) => ( ( ( (conj ( (dotpipp B) (_225 : (eprop B) => C) ) ) ( (dotpipp C) (_226 : (eprop C) => B) ) ) (H3欧0 : (eprop B) => ( (H6 : (eprop (not A) ) => ( (H欧0 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) C) (H1欧1 : (eprop C) => ( (H欧1 : (eprop (not A) ) => ( (H0欧0 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H2欧1 : (eprop B) => H1欧1) ) (H2欧1 : (eprop A) => ( (H0欧1 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) C) (H4欧0 : (eprop C) => ( (H0欧2 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H5欧0 : (eprop B) => ( (H0欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind C) H6欧0) ) (H欧1 H2欧1) ) ) (H6 H2欧1) ) ) ) (H5欧0 : (eprop A) => ( (H0欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind C) H6欧0) ) (H欧1 H2欧1) ) ) (H6 H2欧1) ) ) ) H0欧2) ) (H5 H2欧1) ) ) ) (H4欧0 : (eprop A) => ( (H0欧2 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H5欧0 : (eprop B) => ( (H0欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind C) H6欧0) ) (H欧1 H2欧1) ) ) (H6 H2欧1) ) ) ) (H5欧0 : (eprop A) => ( (H0欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind C) H6欧0) ) (H欧1 H2欧1) ) ) (H6 H2欧1) ) ) ) H0欧2) ) (H5 H2欧1) ) ) ) H0欧1) ) (H4 H2欧1) ) ) ) H0欧0) ) (H2欧0 H1欧1) ) ) (H0 H1欧1) ) ) ) (H1欧1 : (eprop A) => ( (H欧1 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) C) (H4欧0 : (eprop C) => ( (H欧2 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H5欧0 : (eprop B) => ( (H欧3 : (eprop False) => ( (H6欧0 : (eprop (not A) ) => ( (H0欧0 : (eprop False) => ( (H6欧1 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H2欧1 : (eprop B) => ( (False_ind C) H0欧0) ) ) (H2欧1 : (eprop A) => ( (False_ind C) H0欧0) ) ) H6欧1) ) (H2欧0 H4欧0) ) ) (H6欧0 H1欧1) ) ) (H0 H4欧0) ) ) (H6 H1欧1) ) ) ) (H5欧0 : (eprop A) => ( (H欧3 : (eprop False) => ( (H6欧0 : (eprop (not A) ) => ( (H0欧0 : (eprop False) => ( (H6欧1 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H2欧1 : (eprop B) => ( (False_ind C) H0欧0) ) ) (H2欧1 : (eprop A) => ( (False_ind C) H0欧0) ) ) H6欧1) ) (H2欧0 H4欧0) ) ) (H6欧0 H1欧1) ) ) (H0 H4欧0) ) ) (H6 H1欧1) ) ) ) H欧2) ) (H5 H1欧1) ) ) ) (H4欧0 : (eprop A) => ( (H欧2 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H5欧0 : (eprop B) => ( (H欧3 : (eprop False) => ( (False_ind C) H欧3) ) (H6 H1欧1) ) ) ) (H5欧0 : (eprop A) => ( (H欧3 : (eprop False) => ( (False_ind C) H欧3) ) (H6 H1欧1) ) ) ) H欧2) ) (H5 H1欧1) ) ) ) H欧1) ) (H4 H1欧1) ) ) ) H欧0) ) (H1欧0 H3欧0) ) ) (H H3欧0) ) ) ) (H3欧0 : (eprop C) => ( (H6 : (eprop (not A) ) => ( (H0欧0 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) B) (H2欧1 : (eprop B) => ( (H0欧1 : (eprop (not A) ) => ( (H欧0 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) B) (H1欧1 : (eprop C) => H2欧1) ) (H1欧1 : (eprop A) => ( (H欧1 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) B) (H4欧0 : (eprop C) => ( (H欧2 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) B) (H5欧0 : (eprop B) => ( (H欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind B) H6欧0) ) (H0欧1 H1欧1) ) ) (H6 H1欧1) ) ) ) (H5欧0 : (eprop A) => ( (H欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind B) H6欧0) ) (H0欧1 H1欧1) ) ) (H6 H1欧1) ) ) ) H欧2) ) (H5 H1欧1) ) ) ) (H4欧0 : (eprop A) => ( (H欧2 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) B) (H5欧0 : (eprop B) => ( (H欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind B) H6欧0) ) (H0欧1 H1欧1) ) ) (H6 H1欧1) ) ) ) (H5欧0 : (eprop A) => ( (H欧3 : (eprop False) => ( (H6欧0 : (eprop False) => ( (False_ind B) H6欧0) ) (H0欧1 H1欧1) ) ) (H6 H1欧1) ) ) ) H欧2) ) (H5 H1欧1) ) ) ) H欧1) ) (H4 H1欧1) ) ) ) H欧0) ) (H1欧0 H2欧1) ) ) (H H2欧1) ) ) ) (H2欧1 : (eprop A) => ( (H0欧1 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) B) (H4欧0 : (eprop C) => ( (H0欧2 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) B) (H5欧0 : (eprop B) => ( (H0欧3 : (eprop False) => ( (H6欧0 : (eprop (not A) ) => ( (H欧0 : (eprop False) => ( (H6欧1 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) B) (H1欧1 : (eprop C) => ( (False_ind B) H欧0) ) ) (H1欧1 : (eprop A) => ( (False_ind B) H欧0) ) ) H6欧1) ) (H1欧0 H5欧0) ) ) (H6欧0 H2欧1) ) ) (H H5欧0) ) ) (H6 H2欧1) ) ) ) (H5欧0 : (eprop A) => ( (H0欧3 : (eprop False) => ( (False_ind B) H0欧3) ) (H6 H2欧1) ) ) ) H0欧2) ) (H5 H2欧1) ) ) ) (H4欧0 : (eprop A) => ( (H0欧2 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) B) (H5欧0 : (eprop B) => ( (H0欧3 : (eprop False) => ( (H6欧0 : (eprop (not A) ) => ( (H欧0 : (eprop False) => ( (H6欧1 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) B) (H1欧1 : (eprop C) => ( (False_ind B) H欧0) ) ) (H1欧1 : (eprop A) => ( (False_ind B) H欧0) ) ) H6欧1) ) (H1欧0 H5欧0) ) ) (H6欧0 H2欧1) ) ) (H H5欧0) ) ) (H6 H2欧1) ) ) ) (H5欧0 : (eprop A) => ( (H0欧3 : (eprop False) => ( (False_ind B) H0欧3) ) (H6 H2欧1) ) ) ) H0欧2) ) (H5 H2欧1) ) ) ) H0欧1) ) (H4 H2欧1) ) ) ) H0欧0) ) (H2欧0 H3欧0) ) ) (H0 H3欧0) ) ) ) ) (H5 : (eprop A) => (H3 ( ( (or_intror C) A) H5) ) ) ) ) (H2欧0 : (eprop C) => (H3 ( ( (or_introl C) A) H2欧0) ) ) ) ) (H4 : (eprop A) => (H2 ( ( (or_intror B) A) H4) ) ) ) ) (H1欧0 : (eprop B) => (H2 ( ( (or_introl B) A) H1欧0) ) ) ) ) ) ) H1) ) ) (H1 : (eprop ( (iff B) C) ) => ( ( ( ( (and_ind ( (dotpipp B) (_233 : (eprop B) => C) ) ) ( (dotpipp C) (_234 : (eprop C) => B) ) ) ( (iff ( (or B) A) ) ( (or C) A) ) ) (H2 : (eprop ( (dotpipp B) (_238 : (eprop B) => C) ) ) => (H3 : (eprop ( (dotpipp C) (_237 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (or B) A) ) (_235 : (eprop ( (or B) A) ) => ( (or C) A) ) ) ) ( (dotpipp ( (or C) A) ) (_236 : (eprop ( (or C) A) ) => ( (or B) A) ) ) ) (H1欧0 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) ( (or C) A) ) (H4 : (eprop B) => ( (H1欧1 : (eprop (not A) ) => ( (H欧0 : (eprop C) => ( (H2欧0 : (eprop (not A) ) => ( (H0欧0 : (eprop B) => ( ( (or_introl C) A) H欧0) ) (H3 H欧0) ) ) (H0 H欧0) ) ) (H2 H4) ) ) (H H4) ) ) ) (H4 : (eprop A) => ( ( (or_intror C) A) H4) ) ) H1欧0) ) ) (H1欧0 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) ( (or B) A) ) (H4 : (eprop C) => ( (H1欧1 : (eprop (not A) ) => ( (H0欧0 : (eprop B) => ( (H3欧0 : (eprop (not A) ) => ( (H欧0 : (eprop C) => ( ( (or_introl B) A) H0欧0) ) (H2 H0欧0) ) ) (H H0欧0) ) ) (H3 H4) ) ) (H0 H4) ) ) ) (H4 : (eprop A) => ( ( (or_intror B) A) H4) ) ) H1欧0) ) ) ) ) ) H1) ) ) ) ) ) ) ) .
and_iff_compat_l : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_251 : (eprop ( (iff B) C) ) -> (eprop ( (iff ( (and A) B) ) ( (and A) C) ) ) ) ) ) ) .
[] and_iff_compat_l --> (A : (etype dotprop) => (B : (etype dotprop) => (C : (etype dotprop) => (H : (eprop ( (iff B) C) ) => ( ( ( ( (and_ind ( (dotpipp B) (_245 : (eprop B) => C) ) ) ( (dotpipp C) (_246 : (eprop C) => B) ) ) ( (iff ( (and A) B) ) ( (and A) C) ) ) (H0 : (eprop ( (dotpipp B) (_250 : (eprop B) => C) ) ) => (H1 : (eprop ( (dotpipp C) (_249 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (and A) B) ) (_247 : (eprop ( (and A) B) ) => ( (and A) C) ) ) ) ( (dotpipp ( (and A) C) ) (_248 : (eprop ( (and A) C) ) => ( (and A) B) ) ) ) (H欧0 : (eprop ( (and A) B) ) => ( ( ( ( (and_ind A) B) ( (and A) C) ) (H2 : (eprop A) => (H3 : (eprop B) => ( (H欧1 : (eprop C) => ( (H0欧0 : (eprop B) => ( ( ( (conj A) C) H2) H欧1) ) (H1 H欧1) ) ) (H0 H3) ) ) ) ) H欧0) ) ) (H欧0 : (eprop ( (and A) C) ) => ( ( ( ( (and_ind A) C) ( (and A) B) ) (H2 : (eprop A) => (H3 : (eprop C) => ( (H欧1 : (eprop B) => ( (H1欧0 : (eprop C) => ( ( ( (conj A) B) H2) H欧1) ) (H0 H欧1) ) ) (H1 H3) ) ) ) ) H欧0) ) ) ) ) ) H) ) ) ) ) .
and_iff_compat_r : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_258 : (eprop ( (iff B) C) ) -> (eprop ( (iff ( (and B) A) ) ( (and C) A) ) ) ) ) ) ) .
[] and_iff_compat_r --> (A : (etype dotprop) => (B : (etype dotprop) => (C : (etype dotprop) => (H : (eprop ( (iff B) C) ) => ( ( ( ( (and_ind ( (dotpipp B) (_252 : (eprop B) => C) ) ) ( (dotpipp C) (_253 : (eprop C) => B) ) ) ( (iff ( (and B) A) ) ( (and C) A) ) ) (H0 : (eprop ( (dotpipp B) (_257 : (eprop B) => C) ) ) => (H1 : (eprop ( (dotpipp C) (_256 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (and B) A) ) (_254 : (eprop ( (and B) A) ) => ( (and C) A) ) ) ) ( (dotpipp ( (and C) A) ) (_255 : (eprop ( (and C) A) ) => ( (and B) A) ) ) ) (H欧0 : (eprop ( (and B) A) ) => ( ( ( ( (and_ind B) A) ( (and C) A) ) (H2 : (eprop B) => (H3 : (eprop A) => ( (H欧1 : (eprop C) => ( (H0欧0 : (eprop B) => ( ( ( (conj C) A) H欧1) H3) ) (H1 H欧1) ) ) (H0 H2) ) ) ) ) H欧0) ) ) (H欧0 : (eprop ( (and C) A) ) => ( ( ( ( (and_ind C) A) ( (and B) A) ) (H2 : (eprop C) => (H3 : (eprop A) => ( (H欧1 : (eprop B) => ( (H1欧0 : (eprop C) => ( ( ( (conj B) A) H欧1) H3) ) (H0 H欧1) ) ) (H1 H2) ) ) ) ) H欧0) ) ) ) ) ) H) ) ) ) ) .
or_iff_compat_l : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_265 : (eprop ( (iff B) C) ) -> (eprop ( (iff ( (or A) B) ) ( (or A) C) ) ) ) ) ) ) .
[] or_iff_compat_l --> (A : (etype dotprop) => (B : (etype dotprop) => (C : (etype dotprop) => (H : (eprop ( (iff B) C) ) => ( ( ( ( (and_ind ( (dotpipp B) (_259 : (eprop B) => C) ) ) ( (dotpipp C) (_260 : (eprop C) => B) ) ) ( (iff ( (or A) B) ) ( (or A) C) ) ) (H0 : (eprop ( (dotpipp B) (_264 : (eprop B) => C) ) ) => (H1 : (eprop ( (dotpipp C) (_263 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (or A) B) ) (_261 : (eprop ( (or A) B) ) => ( (or A) C) ) ) ) ( (dotpipp ( (or A) C) ) (_262 : (eprop ( (or A) C) ) => ( (or A) B) ) ) ) (H欧0 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) ( (or A) C) ) (H2 : (eprop A) => ( ( (or_introl A) C) H2) ) ) (H2 : (eprop B) => ( (H欧1 : (eprop C) => ( (H0欧0 : (eprop B) => ( ( (or_intror A) C) H欧1) ) (H1 H欧1) ) ) (H0 H2) ) ) ) H欧0) ) ) (H欧0 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) ( (or A) B) ) (H2 : (eprop A) => ( ( (or_introl A) B) H2) ) ) (H2 : (eprop C) => ( (H欧1 : (eprop B) => ( (H1欧0 : (eprop C) => ( ( (or_intror A) B) H欧1) ) (H0 H欧1) ) ) (H1 H2) ) ) ) H欧0) ) ) ) ) ) H) ) ) ) ) .
or_iff_compat_r : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_272 : (eprop ( (iff B) C) ) -> (eprop ( (iff ( (or B) A) ) ( (or C) A) ) ) ) ) ) ) .
[] or_iff_compat_r --> (A : (etype dotprop) => (B : (etype dotprop) => (C : (etype dotprop) => (H : (eprop ( (iff B) C) ) => ( ( ( ( (and_ind ( (dotpipp B) (_266 : (eprop B) => C) ) ) ( (dotpipp C) (_267 : (eprop C) => B) ) ) ( (iff ( (or B) A) ) ( (or C) A) ) ) (H0 : (eprop ( (dotpipp B) (_271 : (eprop B) => C) ) ) => (H1 : (eprop ( (dotpipp C) (_270 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (or B) A) ) (_268 : (eprop ( (or B) A) ) => ( (or C) A) ) ) ) ( (dotpipp ( (or C) A) ) (_269 : (eprop ( (or C) A) ) => ( (or B) A) ) ) ) (H欧0 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) ( (or C) A) ) (H2 : (eprop B) => ( (H欧1 : (eprop C) => ( (H0欧0 : (eprop B) => ( ( (or_introl C) A) H欧1) ) (H1 H欧1) ) ) (H0 H2) ) ) ) (H2 : (eprop A) => ( ( (or_intror C) A) H2) ) ) H欧0) ) ) (H欧0 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) ( (or B) A) ) (H2 : (eprop C) => ( (H欧1 : (eprop B) => ( (H1欧0 : (eprop C) => ( ( (or_introl B) A) H欧1) ) (H0 H欧1) ) ) (H1 H2) ) ) ) (H2 : (eprop A) => ( ( (or_intror B) A) H2) ) ) H欧0) ) ) ) ) ) H) ) ) ) ) .
case_10 : (A : Uprop -> (B : Uprop -> (H : (eprop ( (iff A) B) ) -> (_277 : (eprop ( (and ( (dotpipp A) (_273 : (eprop A) => B) ) ) ( (dotpipp B) (_274 : (eprop B) => A) ) ) ) -> (eprop ( (and ( (dotpipp A) (_275 : (eprop A) => B) ) ) ( (dotpipp B) (_276 : (eprop B) => A) ) ) ) ) ) ) ) .
conj_case_10 : (A : Uprop -> (B : Uprop -> (H : (eprop ( (iff A) B) ) -> (_285 : (_280 : (eprop A) -> (eprop B) ) -> (_284 : (_281 : (eprop B) -> (eprop A) ) -> (eprop ( (and ( (dotpipp A) (_282 : (eprop A) => B) ) ) ( (dotpipp B) (_283 : (eprop B) => A) ) ) ) ) ) ) ) ) .
[A : Uprop, B : Uprop, H : (eprop ( (iff A) B) ) ] ( ( (conj_case_10 A) B) H) --> ( (conj ( (dotpipp A) (_278 : (eprop A) => B) ) ) ( (dotpipp B) (_279 : (eprop B) => A) ) ) .
[A : Uprop, B : Uprop, H : (eprop ( (iff A) B) ) , var_16 : (_286 : (eprop A) -> (eprop B) ) , var_17 : (_287 : (eprop B) -> (eprop A) ) ] ( ( ( (case_10 A) B) H) ( ( ( ( (conj_case_10 A) B) H) var_16) var_17) ) --> ( ( (H欧0 : (eprop ( (dotpipp A) (_291 : (eprop A) => B) ) ) => (H0 : (eprop ( (dotpipp B) (_290 : (eprop B) => A) ) ) => ( ( ( (conj ( (dotpipp A) (_288 : (eprop A) => B) ) ) ( (dotpipp B) (_289 : (eprop B) => A) ) ) H欧0) H0) ) ) var_16) var_17) .
iff_and : (A : Uprop -> (B : Uprop -> (_294 : (eprop ( (iff A) B) ) -> (eprop ( (and ( (dotpipp A) (_292 : (eprop A) => B) ) ) ( (dotpipp B) (_293 : (eprop B) => A) ) ) ) ) ) ) .
[] iff_and --> (A : (etype dotprop) => (B : (etype dotprop) => (H : (eprop ( (iff A) B) ) => ( ( ( (case_10 A) B) H) H) ) ) ) .
iff_to_and : (A : Uprop -> (B : Uprop -> (eprop ( (iff ( (iff A) B) ) ( (and ( (dotpipp A) (_317 : (eprop A) => B) ) ) ( (dotpipp B) (_318 : (eprop B) => A) ) ) ) ) ) ) .
[] iff_to_and --> (A : (etype dotprop) => (B : (etype dotprop) => ( ( ( (conj ( (dotpipp ( (iff A) B) ) (_297 : (eprop ( (iff A) B) ) => ( (and ( (dotpipp A) (_295 : (eprop A) => B) ) ) ( (dotpipp B) (_296 : (eprop B) => A) ) ) ) ) ) ( (dotpipp ( (and ( (dotpipp A) (_298 : (eprop A) => B) ) ) ( (dotpipp B) (_299 : (eprop B) => A) ) ) ) (_300 : (eprop ( (and ( (dotpipp A) (_298 : (eprop A) => B) ) ) ( (dotpipp B) (_299 : (eprop B) => A) ) ) ) => ( (iff A) B) ) ) ) (H : (eprop ( (iff A) B) ) => ( ( ( ( (and_ind ( (dotpipp A) (_301 : (eprop A) => B) ) ) ( (dotpipp B) (_302 : (eprop B) => A) ) ) ( (and ( (dotpipp A) (_303 : (eprop A) => B) ) ) ( (dotpipp B) (_304 : (eprop B) => A) ) ) ) (H0 : (eprop ( (dotpipp A) (_308 : (eprop A) => B) ) ) => (H1 : (eprop ( (dotpipp B) (_307 : (eprop B) => A) ) ) => ( ( ( (conj ( (dotpipp A) (_305 : (eprop A) => B) ) ) ( (dotpipp B) (_306 : (eprop B) => A) ) ) (H欧0 : (eprop A) => ( (H2 : (eprop B) => ( (H0欧0 : (eprop A) => H2) (H1 H2) ) ) (H0 H欧0) ) ) ) (H欧0 : (eprop B) => ( (H2 : (eprop A) => ( (H1欧0 : (eprop B) => H2) (H0 H2) ) ) (H1 H欧0) ) ) ) ) ) ) H) ) ) (H : (eprop ( (and ( (dotpipp A) (_315 : (eprop A) => B) ) ) ( (dotpipp B) (_316 : (eprop B) => A) ) ) ) => ( ( ( ( (and_ind ( (dotpipp A) (_309 : (eprop A) => B) ) ) ( (dotpipp B) (_310 : (eprop B) => A) ) ) ( (iff A) B) ) (H0 : (eprop ( (dotpipp A) (_314 : (eprop A) => B) ) ) => (H1 : (eprop ( (dotpipp B) (_313 : (eprop B) => A) ) ) => ( ( ( (conj ( (dotpipp A) (_311 : (eprop A) => B) ) ) ( (dotpipp B) (_312 : (eprop B) => A) ) ) (H欧0 : (eprop A) => ( (H2 : (eprop B) => ( (H0欧0 : (eprop A) => H2) (H1 H2) ) ) (H0 H欧0) ) ) ) (H欧0 : (eprop B) => ( (H2 : (eprop A) => ( (H1欧0 : (eprop B) => H2) (H0 H2) ) ) (H1 H欧0) ) ) ) ) ) ) H) ) ) ) ) .
IF_then_else : (P : Uprop -> (Q : Uprop -> (R : Uprop -> Uprop) ) ) .
[] IF_then_else --> (P : (etype dotprop) => (Q : (etype dotprop) => (R : (etype dotprop) => ( (or ( (and P) Q) ) ( (and (not P) ) R) ) ) ) ) .
ex : (A : Utype -> (P : (_319 : (etype A) -> Uprop) -> Uprop) ) .
ex_intro : (A : Utype -> (P : (_320 : (etype A) -> Uprop) -> (x : (etype A) -> (_321 : (eprop (P x) ) -> (eprop ( (ex A) P) ) ) ) ) ) .
case_11 : (A : Utype -> (P : (_322 : (etype A) -> Uprop) -> (P欧0 : Uprop -> (f : (x : (etype A) -> (_323 : (eprop (P x) ) -> (eprop P欧0) ) ) -> (e : (eprop ( (ex A) P) ) -> (_324 : (eprop ( (ex A) P) ) -> (eprop P欧0) ) ) ) ) ) ) .
ex_intro_case_11 : (A : Utype -> (P : (_327 : (etype A) -> Uprop) -> (P欧0 : Uprop -> (f : (x : (etype A) -> (_328 : (eprop (P x) ) -> (eprop P欧0) ) ) -> (e : (eprop ( (ex A) P) ) -> (x : (etype A) -> (_329 : (eprop (P x) ) -> (eprop ( (ex A) P) ) ) ) ) ) ) ) ) .
[A : Utype, P : (_330 : (etype A) -> Uprop) , P欧0 : Uprop, f : (x : (etype A) -> (_331 : (eprop (P x) ) -> (eprop P欧0) ) ) , e : (eprop ( (ex A) P) ) ] ( ( ( ( (ex_intro_case_11 A) P) P欧0) f) e) --> ( (ex_intro A) P) .
[A : Utype, P : (_325 : (etype A) -> Uprop) , P欧0 : Uprop, f : (x : (etype A) -> (_326 : (eprop (P x) ) -> (eprop P欧0) ) ) , e : (eprop ( (ex A) P) ) , var_18 : (etype A) , var_19 : (eprop (P var_18) ) ] ( ( ( ( ( (case_11 A) P) P欧0) f) e) ( ( ( ( ( ( (ex_intro_case_11 A) P) P欧0) f) e) var_18) var_19) ) --> ( (f var_18) var_19) .
ex_ind : (A : Utype -> (P : (_334 : (etype A) -> Uprop) -> (P欧0 : Uprop -> (f : (x : (etype A) -> (_335 : (eprop (P x) ) -> (eprop P欧0) ) ) -> (e : (eprop ( (ex A) P) ) -> (eprop P欧0) ) ) ) ) ) .
[] ex_ind --> (A : (etype dottype) => (P : (etype ( (dotpitt A) (_333 : (etype A) => dotprop) ) ) => (P欧0 : (etype dotprop) => (f : (eprop ( (dotpitp A) (x : (etype A) => ( (dotpipp (P x) ) (_332 : (eprop (P x) ) => P欧0) ) ) ) ) => (e : (eprop ( (ex A) P) ) => ( ( ( ( ( (case_11 A) P) P欧0) f) e) e) ) ) ) ) ) .
ex2 : (A : Utype -> (P : (_336 : (etype A) -> Uprop) -> (Q : (_337 : (etype A) -> Uprop) -> Uprop) ) ) .
ex_intro2 : (A : Utype -> (P : (_338 : (etype A) -> Uprop) -> (Q : (_339 : (etype A) -> Uprop) -> (x : (etype A) -> (_341 : (eprop (P x) ) -> (_340 : (eprop (Q x) ) -> (eprop ( ( (ex2 A) P) Q) ) ) ) ) ) ) ) .
case_12 : (A : Utype -> (P : (_342 : (etype A) -> Uprop) -> (Q : (_343 : (etype A) -> Uprop) -> (P欧0 : Uprop -> (f : (x : (etype A) -> (_345 : (eprop (P x) ) -> (_344 : (eprop (Q x) ) -> (eprop P欧0) ) ) ) -> (e : (eprop ( ( (ex2 A) P) Q) ) -> (_346 : (eprop ( ( (ex2 A) P) Q) ) -> (eprop P欧0) ) ) ) ) ) ) ) .
ex_intro2_case_12 : (A : Utype -> (P : (_351 : (etype A) -> Uprop) -> (Q : (_352 : (etype A) -> Uprop) -> (P欧0 : Uprop -> (f : (x : (etype A) -> (_354 : (eprop (P x) ) -> (_353 : (eprop (Q x) ) -> (eprop P欧0) ) ) ) -> (e : (eprop ( ( (ex2 A) P) Q) ) -> (x : (etype A) -> (_356 : (eprop (P x) ) -> (_355 : (eprop (Q x) ) -> (eprop ( ( (ex2 A) P) Q) ) ) ) ) ) ) ) ) ) ) .
[A : Utype, P : (_357 : (etype A) -> Uprop) , Q : (_358 : (etype A) -> Uprop) , P欧0 : Uprop, f : (x : (etype A) -> (_360 : (eprop (P x) ) -> (_359 : (eprop (Q x) ) -> (eprop P欧0) ) ) ) , e : (eprop ( ( (ex2 A) P) Q) ) ] ( ( ( ( ( (ex_intro2_case_12 A) P) Q) P欧0) f) e) --> ( ( (ex_intro2 A) P) Q) .
[A : Utype, P : (_347 : (etype A) -> Uprop) , Q : (_348 : (etype A) -> Uprop) , P欧0 : Uprop, f : (x : (etype A) -> (_350 : (eprop (P x) ) -> (_349 : (eprop (Q x) ) -> (eprop P欧0) ) ) ) , e : (eprop ( ( (ex2 A) P) Q) ) , var_20 : (etype A) , var_21 : (eprop (P var_20) ) , var_22 : (eprop (Q var_20) ) ] ( ( ( ( ( ( (case_12 A) P) Q) P欧0) f) e) ( ( ( ( ( ( ( ( (ex_intro2_case_12 A) P) Q) P欧0) f) e) var_20) var_21) var_22) ) --> ( ( (f var_20) var_21) var_22) .
ex2_ind : (A : Utype -> (P : (_365 : (etype A) -> Uprop) -> (Q : (_366 : (etype A) -> Uprop) -> (P欧0 : Uprop -> (f : (x : (etype A) -> (_368 : (eprop (P x) ) -> (_367 : (eprop (Q x) ) -> (eprop P欧0) ) ) ) -> (e : (eprop ( ( (ex2 A) P) Q) ) -> (eprop P欧0) ) ) ) ) ) ) .
[] ex2_ind --> (A : (etype dottype) => (P : (etype ( (dotpitt A) (_364 : (etype A) => dotprop) ) ) => (Q : (etype ( (dotpitt A) (_363 : (etype A) => dotprop) ) ) => (P欧0 : (etype dotprop) => (f : (eprop ( (dotpitp A) (x : (etype A) => ( (dotpipp (P x) ) (_362 : (eprop (P x) ) => ( (dotpipp (Q x) ) (_361 : (eprop (Q x) ) => P欧0) ) ) ) ) ) ) => (e : (eprop ( ( (ex2 A) P) Q) ) => ( ( ( ( ( ( (case_12 A) P) Q) P欧0) f) e) e) ) ) ) ) ) ) .
all : (A : Utype -> (P : (_370 : (etype A) -> Uprop) -> Uprop) ) .
[] all --> (A : (etype dottype) => (P : (etype ( (dotpitt A) (_369 : (etype A) => dotprop) ) ) => ( (dotpitp A) (x : (etype A) => (P x) ) ) ) ) .
inst : (A : Utype -> (P : (_372 : (etype A) -> Uprop) -> (x : (etype A) -> (_373 : (eprop ( (all A) (x欧0 : (etype A) => (P x欧0) ) ) ) -> (eprop (P x) ) ) ) ) ) .
[] inst --> (A : (etype dottype) => (P : (etype ( (dotpitt A) (_371 : (etype A) => dotprop) ) ) => (x : (etype A) => (H : (eprop ( (dotpitp A) (x欧0 : (etype A) => (P x欧0) ) ) ) => (H x) ) ) ) ) .
gen : (A : Utype -> (P : (_376 : (etype A) -> Uprop) -> (B : Uprop -> (f : (y : (etype A) -> (_377 : (eprop B) -> (eprop (P y) ) ) ) -> (_378 : (eprop B) -> (eprop ( (all A) P) ) ) ) ) ) ) .
[] gen --> (A : (etype dottype) => (P : (etype ( (dotpitt A) (_375 : (etype A) => dotprop) ) ) => (B : (etype dotprop) => (f : (eprop ( (dotpitp A) (y : (etype A) => ( (dotpipp B) (_374 : (eprop B) => (P y) ) ) ) ) ) => (H : (eprop B) => (x : (etype A) => ( (f x) H) ) ) ) ) ) ) .
eq : (A : Utype -> (x : (etype A) -> (_379 : (etype A) -> Uprop) ) ) .
refl_equal : (A : Utype -> (x : (etype A) -> (eprop ( ( (eq A) x) x) ) ) ) .
case_13 : (A : Utype -> (x : (etype A) -> (P : (_380 : (etype A) -> Utype) -> (f : (etype (P x) ) -> (y : (etype A) -> (e : (eprop ( ( (eq A) x) y) ) -> (y欧0 : (etype A) -> (_381 : (eprop ( ( (eq A) x) y欧0) ) -> (etype (P y欧0) ) ) ) ) ) ) ) ) ) .
refl_equal_case_13 : (A : Utype -> (x : (etype A) -> (P : (_383 : (etype A) -> Utype) -> (f : (etype (P x) ) -> (y : (etype A) -> (e : (eprop ( ( (eq A) x) y) ) -> (eprop ( ( (eq A) x) x) ) ) ) ) ) ) ) .
[A : Utype, x : (etype A) , P : (_384 : (etype A) -> Utype) , f : (etype (P x) ) , y : (etype A) , e : (eprop ( ( (eq A) x) y) ) ] ( ( ( ( ( (refl_equal_case_13 A) x) P) f) y) e) --> ( (refl_equal A) x) .
[A : Utype, x : (etype A) , P : (_382 : (etype A) -> Utype) , f : (etype (P x) ) , y : (etype A) , e : (eprop ( ( (eq A) x) y) ) ] ( ( ( ( ( ( ( (case_13 A) x) P) f) y) e) x) ( ( ( ( ( (refl_equal_case_13 A) x) P) f) y) e) ) --> f.
eq_rect : (A : Utype -> (x : (etype A) -> (P : (_386 : (etype A) -> Utype) -> (f : (etype (P x) ) -> (y : (etype A) -> (e : (eprop ( ( (eq A) x) y) ) -> (etype (P y) ) ) ) ) ) ) ) .
[] eq_rect --> (A : (etype dottype) => (x : (etype A) => (P : (etype ( (dotpitt A) (_385 : (etype A) => dottype) ) ) => (f : (etype (P x) ) => (y : (etype A) => (e : (eprop ( ( (eq A) x) y) ) => ( ( ( ( ( ( ( (case_13 A) x) P) f) y) e) y) e) ) ) ) ) ) ) .
eq_ind : (A : Utype -> (x : (etype A) -> (P : (_388 : (etype A) -> Uprop) -> (f : (eprop (P x) ) -> (y : (etype A) -> (e : (eprop ( ( (eq A) x) y) ) -> (eprop (P y) ) ) ) ) ) ) ) .
[] eq_ind --> (A : (etype dottype) => (x : (etype A) => (P : (etype ( (dotpitt A) (_387 : (etype A) => dotprop) ) ) => ( ( (eq_rect A) x) P) ) ) ) .
eq_rec : (A : Utype -> (x : (etype A) -> (P : (_390 : (etype A) -> Uset) -> (f : (eset (P x) ) -> (y : (etype A) -> (e : (eprop ( ( (eq A) x) y) ) -> (eset (P y) ) ) ) ) ) ) ) .
[] eq_rec --> (A : (etype dottype) => (x : (etype A) => (P : (etype ( (dotpitt A) (_389 : (etype A) => dotset) ) ) => ( ( (eq_rect A) x) P) ) ) ) .
case_14 : (A : Uprop -> (C : Uprop -> (h1 : (eprop A) -> (h2 : (_391 : (eprop A) -> (eprop False) ) -> (f : (eprop False) -> (_392 : (eprop False) -> (eprop C) ) ) ) ) ) ) .
absurd : (A : Uprop -> (C : Uprop -> (_396 : (eprop A) -> (_395 : (eprop (not A) ) -> (eprop C) ) ) ) ) .
[] absurd --> (A : (etype dotprop) => (C : (etype dotprop) => (h1 : (eprop A) => (h2 : (eprop ( (dotpipp A) (_394 : (eprop A) => False) ) ) => ( (f : (eprop False) => ( ( ( ( ( (case_14 A) C) h1) h2) f) f) ) (h2 h1) ) ) ) ) ) .
case_15 : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (H : (eprop ( ( (eq A) x) y) ) -> (y欧0 : (etype A) -> (_397 : (eprop ( ( (eq A) x) y欧0) ) -> (eprop ( ( (eq A) y欧0) x) ) ) ) ) ) ) ) .
refl_equal_case_15 : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (H : (eprop ( ( (eq A) x) y) ) -> (eprop ( ( (eq A) x) x) ) ) ) ) ) .
[A : Utype, x : (etype A) , y : (etype A) , H : (eprop ( ( (eq A) x) y) ) ] ( ( ( (refl_equal_case_15 A) x) y) H) --> ( (refl_equal A) x) .
[A : Utype, x : (etype A) , y : (etype A) , H : (eprop ( ( (eq A) x) y) ) ] ( ( ( ( ( (case_15 A) x) y) H) x) ( ( ( (refl_equal_case_15 A) x) y) H) ) --> ( (refl_equal A) x) .
sym_eq : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (_398 : (eprop ( ( (eq A) x) y) ) -> (eprop ( ( (eq A) y) x) ) ) ) ) ) .
[] sym_eq --> (A : (etype dottype) => (x : (etype A) => (y : (etype A) => (H : (eprop ( ( (eq A) x) y) ) => ( ( ( ( ( (case_15 A) x) y) H) y) H) ) ) ) ) .
case_16 : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (z : (etype A) -> (H : (eprop ( ( (eq A) x) y) ) -> (H0 : (eprop ( ( (eq A) y) z) ) -> (y欧0 : (etype A) -> (_399 : (eprop ( ( (eq A) y) y欧0) ) -> (eprop ( ( (eq A) x) y欧0) ) ) ) ) ) ) ) ) ) .
refl_equal_case_16 : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (z : (etype A) -> (H : (eprop ( ( (eq A) x) y) ) -> (H0 : (eprop ( ( (eq A) y) z) ) -> (eprop ( ( (eq A) y) y) ) ) ) ) ) ) ) .
[A : Utype, x : (etype A) , y : (etype A) , z : (etype A) , H : (eprop ( ( (eq A) x) y) ) , H0 : (eprop ( ( (eq A) y) z) ) ] ( ( ( ( ( (refl_equal_case_16 A) x) y) z) H) H0) --> ( (refl_equal A) y) .
[A : Utype, x : (etype A) , y : (etype A) , z : (etype A) , H : (eprop ( ( (eq A) x) y) ) , H0 : (eprop ( ( (eq A) y) z) ) ] ( ( ( ( ( ( ( (case_16 A) x) y) z) H) H0) y) ( ( ( ( ( (refl_equal_case_16 A) x) y) z) H) H0) ) --> H.
trans_eq : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (z : (etype A) -> (_401 : (eprop ( ( (eq A) x) y) ) -> (_400 : (eprop ( ( (eq A) y) z) ) -> (eprop ( ( (eq A) x) z) ) ) ) ) ) ) ) .
[] trans_eq --> (A : (etype dottype) => (x : (etype A) => (y : (etype A) => (z : (etype A) => (H : (eprop ( ( (eq A) x) y) ) => (H0 : (eprop ( ( (eq A) y) z) ) => ( ( ( ( ( ( ( (case_16 A) x) y) z) H) H0) z) H0) ) ) ) ) ) ) .
case_17 : (A : Utype -> (B : Utype -> (f : (_402 : (etype A) -> (etype B) ) -> (x : (etype A) -> (y : (etype A) -> (H : (eprop ( ( (eq A) x) y) ) -> (y欧0 : (etype A) -> (_403 : (eprop ( ( (eq A) x) y欧0) ) -> (eprop ( ( (eq B) (f x) ) (f y欧0) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_17 : (A : Utype -> (B : Utype -> (f : (_405 : (etype A) -> (etype B) ) -> (x : (etype A) -> (y : (etype A) -> (H : (eprop ( ( (eq A) x) y) ) -> (eprop ( ( (eq A) x) x) ) ) ) ) ) ) ) .
[A : Utype, B : Utype, f : (_406 : (etype A) -> (etype B) ) , x : (etype A) , y : (etype A) , H : (eprop ( ( (eq A) x) y) ) ] ( ( ( ( ( (refl_equal_case_17 A) B) f) x) y) H) --> ( (refl_equal A) x) .
[A : Utype, B : Utype, f : (_404 : (etype A) -> (etype B) ) , x : (etype A) , y : (etype A) , H : (eprop ( ( (eq A) x) y) ) ] ( ( ( ( ( ( ( (case_17 A) B) f) x) y) H) x) ( ( ( ( ( (refl_equal_case_17 A) B) f) x) y) H) ) --> ( (refl_equal B) (f x) ) .
f_equal : (A : Utype -> (B : Utype -> (f : (_408 : (etype A) -> (etype B) ) -> (x : (etype A) -> (y : (etype A) -> (_409 : (eprop ( ( (eq A) x) y) ) -> (eprop ( ( (eq B) (f x) ) (f y) ) ) ) ) ) ) ) ) .
[] f_equal --> (A : (etype dottype) => (B : (etype dottype) => (f : (etype ( (dotpitt A) (_407 : (etype A) => B) ) ) => (x : (etype A) => (y : (etype A) => (H : (eprop ( ( (eq A) x) y) ) => ( ( ( ( ( ( ( (case_17 A) B) f) x) y) H) y) H) ) ) ) ) ) ) .
case_18 : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (h1 : (eprop (not ( ( (eq A) x) y) ) ) -> (h2 : (eprop ( ( (eq A) y) x) ) -> (y欧0 : (etype A) -> (_410 : (eprop ( ( (eq A) y) y欧0) ) -> (h1欧0 : (eprop (not ( ( (eq A) y欧0) y) ) ) -> (eprop ( ( (eq A) y欧0) y) ) ) ) ) ) ) ) ) ) .
refl_equal_case_18 : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (h1 : (eprop (not ( ( (eq A) x) y) ) ) -> (h2 : (eprop ( ( (eq A) y) x) ) -> (eprop ( ( (eq A) y) y) ) ) ) ) ) ) .
[A : Utype, x : (etype A) , y : (etype A) , h1 : (eprop (not ( ( (eq A) x) y) ) ) , h2 : (eprop ( ( (eq A) y) x) ) ] ( ( ( ( (refl_equal_case_18 A) x) y) h1) h2) --> ( (refl_equal A) y) .
[A : Utype, x : (etype A) , y : (etype A) , h1 : (eprop (not ( ( (eq A) x) y) ) ) , h2 : (eprop ( ( (eq A) y) x) ) ] ( ( ( ( ( ( (case_18 A) x) y) h1) h2) y) ( ( ( ( (refl_equal_case_18 A) x) y) h1) h2) ) --> (h1欧0 : (eprop (not ( ( (eq A) y) y) ) ) => ( (refl_equal A) y) ) .
sym_not_eq : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (_411 : (eprop (not ( ( (eq A) x) y) ) ) -> (eprop (not ( ( (eq A) y) x) ) ) ) ) ) ) .
[] sym_not_eq --> (A : (etype dottype) => (x : (etype A) => (y : (etype A) => (h1 : (eprop (not ( ( (eq A) x) y) ) ) => (h2 : (eprop ( ( (eq A) y) x) ) => (h1 ( ( ( ( ( ( ( (case_18 A) x) y) h1) h2) x) h2) h1) ) ) ) ) ) ) .
sym_equal : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (_412 : (eprop ( ( (eq A) x) y) ) -> (eprop ( ( (eq A) y) x) ) ) ) ) ) .
[] sym_equal --> (A : (etype dottype) => (x : (etype A) => (y : (etype A) => ( ( (sym_eq A) x) y) ) ) ) .
sym_not_equal : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (_413 : (eprop (not ( ( (eq A) x) y) ) ) -> (eprop (not ( ( (eq A) y) x) ) ) ) ) ) ) .
[] sym_not_equal --> (A : (etype dottype) => (x : (etype A) => (y : (etype A) => ( ( (sym_not_eq A) x) y) ) ) ) .
trans_equal : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (z : (etype A) -> (_415 : (eprop ( ( (eq A) x) y) ) -> (_414 : (eprop ( ( (eq A) y) z) ) -> (eprop ( ( (eq A) x) z) ) ) ) ) ) ) ) .
[] trans_equal --> (A : (etype dottype) => (x : (etype A) => (y : (etype A) => (z : (etype A) => ( ( ( (trans_eq A) x) y) z) ) ) ) ) .
eq_ind_r : (A : Utype -> (x : (etype A) -> (P : (_417 : (etype A) -> Uprop) -> (_419 : (eprop (P x) ) -> (y : (etype A) -> (_418 : (eprop ( ( (eq A) y) x) ) -> (eprop (P y) ) ) ) ) ) ) ) .
[] eq_ind_r --> (A : (etype dottype) => (x : (etype A) => (P : (etype ( (dotpitt A) (_416 : (etype A) => dotprop) ) ) => (H : (eprop (P x) ) => (y : (etype A) => (H0 : (eprop ( ( (eq A) y) x) ) => ( ( ( ( ( (eq_ind A) x) (y欧0 : (etype A) => (P y欧0) ) ) H) y) ( ( ( (sym_eq A) y) x) H0) ) ) ) ) ) ) ) .
eq_rec_r : (A : Utype -> (x : (etype A) -> (P : (_421 : (etype A) -> Uset) -> (_423 : (eset (P x) ) -> (y : (etype A) -> (_422 : (eprop ( ( (eq A) y) x) ) -> (eset (P y) ) ) ) ) ) ) ) .
[] eq_rec_r --> (A : (etype dottype) => (x : (etype A) => (P : (etype ( (dotpitt A) (_420 : (etype A) => dotset) ) ) => (H : (eset (P x) ) => (y : (etype A) => (H0 : (eprop ( ( (eq A) y) x) ) => ( ( ( ( ( (eq_rec A) x) (y欧0 : (etype A) => (P y欧0) ) ) H) y) ( ( ( (sym_eq A) y) x) H0) ) ) ) ) ) ) ) .
eq_rect_r : (A : Utype -> (x : (etype A) -> (P : (_425 : (etype A) -> Utype) -> (_427 : (etype (P x) ) -> (y : (etype A) -> (_426 : (eprop ( ( (eq A) y) x) ) -> (etype (P y) ) ) ) ) ) ) ) .
[] eq_rect_r --> (A : (etype dottype) => (x : (etype A) => (P : (etype ( (dotpitt A) (_424 : (etype A) => dottype) ) ) => (H : (etype (P x) ) => (y : (etype A) => (H0 : (eprop ( ( (eq A) y) x) ) => ( ( ( ( ( (eq_rect A) x) (y欧0 : (etype A) => (P y欧0) ) ) H) y) ( ( ( (sym_eq A) y) x) H0) ) ) ) ) ) ) ) .
case_19 : (A1 : Utype -> (A2 : Utype -> (B : Utype -> (f : (_429 : (etype A1) -> (_428 : (etype A2) -> (etype B) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (y : (etype A1) -> (_431 : (eprop ( ( (eq A1) x1) y) ) -> (_430 : (eprop ( ( (eq A2) x2) y2) ) -> (eprop ( ( (eq B) ( (f x1) x2) ) ( (f y) y2) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_19 : (A1 : Utype -> (A2 : Utype -> (B : Utype -> (f : (_435 : (etype A1) -> (_434 : (etype A2) -> (etype B) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (eprop ( ( (eq A1) x1) x1) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, B : Utype, f : (_437 : (etype A1) -> (_436 : (etype A2) -> (etype B) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , H : (eprop ( ( (eq A1) x1) y1) ) ] ( ( ( ( ( ( ( ( (refl_equal_case_19 A1) A2) B) f) x1) y1) x2) y2) H) --> ( (refl_equal A1) x1) .
case_20 : (A1 : Utype -> (A2 : Utype -> (B : Utype -> (f : (_439 : (etype A1) -> (_438 : (etype A2) -> (etype B) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (y : (etype A2) -> (_440 : (eprop ( ( (eq A2) x2) y) ) -> (eprop ( ( (eq B) ( (f x1) x2) ) ( (f x1) y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_20 : (A1 : Utype -> (A2 : Utype -> (B : Utype -> (f : (_444 : (etype A1) -> (_443 : (etype A2) -> (etype B) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (eprop ( ( (eq A2) x2) x2) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, B : Utype, f : (_446 : (etype A1) -> (_445 : (etype A2) -> (etype B) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) ] ( ( ( ( ( ( ( ( ( (refl_equal_case_20 A1) A2) B) f) x1) y1) x2) y2) H) H欧0) --> ( (refl_equal A2) x2) .
[A1 : Utype, A2 : Utype, B : Utype, f : (_442 : (etype A1) -> (_441 : (etype A2) -> (etype B) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) ] ( ( ( ( ( ( ( ( ( ( ( (case_20 A1) A2) B) f) x1) y1) x2) y2) H) H欧0) x2) ( ( ( ( ( ( ( ( ( (refl_equal_case_20 A1) A2) B) f) x1) y1) x2) y2) H) H欧0) ) --> ( (refl_equal B) ( (f x1) x2) ) .
[A1 : Utype, A2 : Utype, B : Utype, f : (_433 : (etype A1) -> (_432 : (etype A2) -> (etype B) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , H : (eprop ( ( (eq A1) x1) y1) ) ] ( ( ( ( ( ( ( ( ( ( (case_19 A1) A2) B) f) x1) y1) x2) y2) H) x1) ( ( ( ( ( ( ( ( (refl_equal_case_19 A1) A2) B) f) x1) y1) x2) y2) H) ) --> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) => ( ( ( ( ( ( ( ( ( ( ( (case_20 A1) A2) B) f) x1) y1) x2) y2) H) H欧0) y2) H欧0) ) .
f_equal2 : (A1 : Utype -> (A2 : Utype -> (B : Utype -> (f : (_450 : (etype A1) -> (_449 : (etype A2) -> (etype B) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (_452 : (eprop ( ( (eq A1) x1) y1) ) -> (_451 : (eprop ( ( (eq A2) x2) y2) ) -> (eprop ( ( (eq B) ( (f x1) x2) ) ( (f y1) y2) ) ) ) ) ) ) ) ) ) ) ) ) .
[] f_equal2 --> (A1 : (etype dottype) => (A2 : (etype dottype) => (B : (etype dottype) => (f : (etype ( (dotpitt A1) (_448 : (etype A1) => ( (dotpitt A2) (_447 : (etype A2) => B) ) ) ) ) => (x1 : (etype A1) => (y1 : (etype A1) => (x2 : (etype A2) => (y2 : (etype A2) => (H : (eprop ( ( (eq A1) x1) y1) ) => ( ( ( ( ( ( ( ( ( ( (case_19 A1) A2) B) f) x1) y1) x2) y2) H) y1) H) ) ) ) ) ) ) ) ) ) .
case_21 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (B : Utype -> (f : (_455 : (etype A1) -> (_454 : (etype A2) -> (_453 : (etype A3) -> (etype B) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (y : (etype A1) -> (_458 : (eprop ( ( (eq A1) x1) y) ) -> (_457 : (eprop ( ( (eq A2) x2) y2) ) -> (_456 : (eprop ( ( (eq A3) x3) y3) ) -> (eprop ( ( (eq B) ( ( (f x1) x2) x3) ) ( ( (f y) y2) y3) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_21 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (B : Utype -> (f : (_464 : (etype A1) -> (_463 : (etype A2) -> (_462 : (etype A3) -> (etype B) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (eprop ( ( (eq A1) x1) x1) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, B : Utype, f : (_467 : (etype A1) -> (_466 : (etype A2) -> (_465 : (etype A3) -> (etype B) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , H : (eprop ( ( (eq A1) x1) y1) ) ] ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_21 A1) A2) A3) B) f) x1) y1) x2) y2) x3) y3) H) --> ( (refl_equal A1) x1) .
case_22 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (B : Utype -> (f : (_470 : (etype A1) -> (_469 : (etype A2) -> (_468 : (etype A3) -> (etype B) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (y : (etype A2) -> (_472 : (eprop ( ( (eq A2) x2) y) ) -> (_471 : (eprop ( ( (eq A3) x3) y3) ) -> (eprop ( ( (eq B) ( ( (f x1) x2) x3) ) ( ( (f x1) y) y3) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_22 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (B : Utype -> (f : (_478 : (etype A1) -> (_477 : (etype A2) -> (_476 : (etype A3) -> (etype B) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (eprop ( ( (eq A2) x2) x2) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, B : Utype, f : (_481 : (etype A1) -> (_480 : (etype A2) -> (_479 : (etype A3) -> (etype B) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) ] ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_22 A1) A2) A3) B) f) x1) y1) x2) y2) x3) y3) H) H欧0) --> ( (refl_equal A2) x2) .
case_23 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (B : Utype -> (f : (_484 : (etype A1) -> (_483 : (etype A2) -> (_482 : (etype A3) -> (etype B) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) -> (y : (etype A3) -> (_485 : (eprop ( ( (eq A3) x3) y) ) -> (eprop ( ( (eq B) ( ( (f x1) x2) x3) ) ( ( (f x1) x2) y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_23 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (B : Utype -> (f : (_491 : (etype A1) -> (_490 : (etype A2) -> (_489 : (etype A3) -> (etype B) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) -> (eprop ( ( (eq A3) x3) x3) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, B : Utype, f : (_494 : (etype A1) -> (_493 : (etype A2) -> (_492 : (etype A3) -> (etype B) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) , H欧1 : (eprop ( ( (eq A3) x3) y3) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_23 A1) A2) A3) B) f) x1) y1) x2) y2) x3) y3) H) H欧0) H欧1) --> ( (refl_equal A3) x3) .
[A1 : Utype, A2 : Utype, A3 : Utype, B : Utype, f : (_488 : (etype A1) -> (_487 : (etype A2) -> (_486 : (etype A3) -> (etype B) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) , H欧1 : (eprop ( ( (eq A3) x3) y3) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_23 A1) A2) A3) B) f) x1) y1) x2) y2) x3) y3) H) H欧0) H欧1) x3) ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_23 A1) A2) A3) B) f) x1) y1) x2) y2) x3) y3) H) H欧0) H欧1) ) --> ( (refl_equal B) ( ( (f x1) x2) x3) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, B : Utype, f : (_475 : (etype A1) -> (_474 : (etype A2) -> (_473 : (etype A3) -> (etype B) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_22 A1) A2) A3) B) f) x1) y1) x2) y2) x3) y3) H) H欧0) x2) ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_22 A1) A2) A3) B) f) x1) y1) x2) y2) x3) y3) H) H欧0) ) --> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) => ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_23 A1) A2) A3) B) f) x1) y1) x2) y2) x3) y3) H) H欧0) H欧1) y3) H欧1) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, B : Utype, f : (_461 : (etype A1) -> (_460 : (etype A2) -> (_459 : (etype A3) -> (etype B) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , H : (eprop ( ( (eq A1) x1) y1) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( (case_21 A1) A2) A3) B) f) x1) y1) x2) y2) x3) y3) H) x1) ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_21 A1) A2) A3) B) f) x1) y1) x2) y2) x3) y3) H) ) --> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) => ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_22 A1) A2) A3) B) f) x1) y1) x2) y2) x3) y3) H) H欧0) y2) H欧0) ) .
f_equal3 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (B : Utype -> (f : (_500 : (etype A1) -> (_499 : (etype A2) -> (_498 : (etype A3) -> (etype B) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (_503 : (eprop ( ( (eq A1) x1) y1) ) -> (_502 : (eprop ( ( (eq A2) x2) y2) ) -> (_501 : (eprop ( ( (eq A3) x3) y3) ) -> (eprop ( ( (eq B) ( ( (f x1) x2) x3) ) ( ( (f y1) y2) y3) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[] f_equal3 --> (A1 : (etype dottype) => (A2 : (etype dottype) => (A3 : (etype dottype) => (B : (etype dottype) => (f : (etype ( (dotpitt A1) (_497 : (etype A1) => ( (dotpitt A2) (_496 : (etype A2) => ( (dotpitt A3) (_495 : (etype A3) => B) ) ) ) ) ) ) => (x1 : (etype A1) => (y1 : (etype A1) => (x2 : (etype A2) => (y2 : (etype A2) => (x3 : (etype A3) => (y3 : (etype A3) => (H : (eprop ( ( (eq A1) x1) y1) ) => ( ( ( ( ( ( ( ( ( ( ( ( ( (case_21 A1) A2) A3) B) f) x1) y1) x2) y2) x3) y3) H) y1) H) ) ) ) ) ) ) ) ) ) ) ) ) .
case_24 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (B : Utype -> (f : (_507 : (etype A1) -> (_506 : (etype A2) -> (_505 : (etype A3) -> (_504 : (etype A4) -> (etype B) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (y : (etype A1) -> (_511 : (eprop ( ( (eq A1) x1) y) ) -> (_510 : (eprop ( ( (eq A2) x2) y2) ) -> (_509 : (eprop ( ( (eq A3) x3) y3) ) -> (_508 : (eprop ( ( (eq A4) x4) y4) ) -> (eprop ( ( (eq B) ( ( ( (f x1) x2) x3) x4) ) ( ( ( (f y) y2) y3) y4) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_24 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (B : Utype -> (f : (_519 : (etype A1) -> (_518 : (etype A2) -> (_517 : (etype A3) -> (_516 : (etype A4) -> (etype B) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (eprop ( ( (eq A1) x1) x1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, B : Utype, f : (_523 : (etype A1) -> (_522 : (etype A2) -> (_521 : (etype A3) -> (_520 : (etype A4) -> (etype B) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , H : (eprop ( ( (eq A1) x1) y1) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_24 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) --> ( (refl_equal A1) x1) .
case_25 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (B : Utype -> (f : (_527 : (etype A1) -> (_526 : (etype A2) -> (_525 : (etype A3) -> (_524 : (etype A4) -> (etype B) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (y : (etype A2) -> (_530 : (eprop ( ( (eq A2) x2) y) ) -> (_529 : (eprop ( ( (eq A3) x3) y3) ) -> (_528 : (eprop ( ( (eq A4) x4) y4) ) -> (eprop ( ( (eq B) ( ( ( (f x1) x2) x3) x4) ) ( ( ( (f x1) y) y3) y4) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_25 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (B : Utype -> (f : (_538 : (etype A1) -> (_537 : (etype A2) -> (_536 : (etype A3) -> (_535 : (etype A4) -> (etype B) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (eprop ( ( (eq A2) x2) x2) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, B : Utype, f : (_542 : (etype A1) -> (_541 : (etype A2) -> (_540 : (etype A3) -> (_539 : (etype A4) -> (etype B) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_25 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) H欧0) --> ( (refl_equal A2) x2) .
case_26 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (B : Utype -> (f : (_546 : (etype A1) -> (_545 : (etype A2) -> (_544 : (etype A3) -> (_543 : (etype A4) -> (etype B) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) -> (y : (etype A3) -> (_548 : (eprop ( ( (eq A3) x3) y) ) -> (_547 : (eprop ( ( (eq A4) x4) y4) ) -> (eprop ( ( (eq B) ( ( ( (f x1) x2) x3) x4) ) ( ( ( (f x1) x2) y) y4) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_26 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (B : Utype -> (f : (_556 : (etype A1) -> (_555 : (etype A2) -> (_554 : (etype A3) -> (_553 : (etype A4) -> (etype B) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) -> (eprop ( ( (eq A3) x3) x3) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, B : Utype, f : (_560 : (etype A1) -> (_559 : (etype A2) -> (_558 : (etype A3) -> (_557 : (etype A4) -> (etype B) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) , H欧1 : (eprop ( ( (eq A3) x3) y3) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_26 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) H欧0) H欧1) --> ( (refl_equal A3) x3) .
case_27 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (B : Utype -> (f : (_564 : (etype A1) -> (_563 : (etype A2) -> (_562 : (etype A3) -> (_561 : (etype A4) -> (etype B) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) -> (H欧2 : (eprop ( ( (eq A4) x4) y4) ) -> (y : (etype A4) -> (_565 : (eprop ( ( (eq A4) x4) y) ) -> (eprop ( ( (eq B) ( ( ( (f x1) x2) x3) x4) ) ( ( ( (f x1) x2) x3) y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_27 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (B : Utype -> (f : (_573 : (etype A1) -> (_572 : (etype A2) -> (_571 : (etype A3) -> (_570 : (etype A4) -> (etype B) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) -> (H欧2 : (eprop ( ( (eq A4) x4) y4) ) -> (eprop ( ( (eq A4) x4) x4) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, B : Utype, f : (_577 : (etype A1) -> (_576 : (etype A2) -> (_575 : (etype A3) -> (_574 : (etype A4) -> (etype B) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) , H欧1 : (eprop ( ( (eq A3) x3) y3) ) , H欧2 : (eprop ( ( (eq A4) x4) y4) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_27 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) H欧0) H欧1) H欧2) --> ( (refl_equal A4) x4) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, B : Utype, f : (_569 : (etype A1) -> (_568 : (etype A2) -> (_567 : (etype A3) -> (_566 : (etype A4) -> (etype B) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) , H欧1 : (eprop ( ( (eq A3) x3) y3) ) , H欧2 : (eprop ( ( (eq A4) x4) y4) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_27 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) H欧0) H欧1) H欧2) x4) ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_27 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) H欧0) H欧1) H欧2) ) --> ( (refl_equal B) ( ( ( (f x1) x2) x3) x4) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, B : Utype, f : (_552 : (etype A1) -> (_551 : (etype A2) -> (_550 : (etype A3) -> (_549 : (etype A4) -> (etype B) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) , H欧1 : (eprop ( ( (eq A3) x3) y3) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_26 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) H欧0) H欧1) x3) ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_26 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) H欧0) H欧1) ) --> (H欧2 : (eprop ( ( (eq A4) x4) y4) ) => ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_27 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) H欧0) H欧1) H欧2) y4) H欧2) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, B : Utype, f : (_534 : (etype A1) -> (_533 : (etype A2) -> (_532 : (etype A3) -> (_531 : (etype A4) -> (etype B) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_25 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) H欧0) x2) ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_25 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) H欧0) ) --> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) => ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_26 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) H欧0) H欧1) y3) H欧1) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, B : Utype, f : (_515 : (etype A1) -> (_514 : (etype A2) -> (_513 : (etype A3) -> (_512 : (etype A4) -> (etype B) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , H : (eprop ( ( (eq A1) x1) y1) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_24 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) x1) ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_24 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) ) --> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) => ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_25 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) H欧0) y2) H欧0) ) .
f_equal4 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (B : Utype -> (f : (_585 : (etype A1) -> (_584 : (etype A2) -> (_583 : (etype A3) -> (_582 : (etype A4) -> (etype B) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (_589 : (eprop ( ( (eq A1) x1) y1) ) -> (_588 : (eprop ( ( (eq A2) x2) y2) ) -> (_587 : (eprop ( ( (eq A3) x3) y3) ) -> (_586 : (eprop ( ( (eq A4) x4) y4) ) -> (eprop ( ( (eq B) ( ( ( (f x1) x2) x3) x4) ) ( ( ( (f y1) y2) y3) y4) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[] f_equal4 --> (A1 : (etype dottype) => (A2 : (etype dottype) => (A3 : (etype dottype) => (A4 : (etype dottype) => (B : (etype dottype) => (f : (etype ( (dotpitt A1) (_581 : (etype A1) => ( (dotpitt A2) (_580 : (etype A2) => ( (dotpitt A3) (_579 : (etype A3) => ( (dotpitt A4) (_578 : (etype A4) => B) ) ) ) ) ) ) ) ) => (x1 : (etype A1) => (y1 : (etype A1) => (x2 : (etype A2) => (y2 : (etype A2) => (x3 : (etype A3) => (y3 : (etype A3) => (x4 : (etype A4) => (y4 : (etype A4) => (H : (eprop ( ( (eq A1) x1) y1) ) => ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_24 A1) A2) A3) A4) B) f) x1) y1) x2) y2) x3) y3) x4) y4) H) y1) H) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
case_28 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (A5 : Utype -> (B : Utype -> (f : (_594 : (etype A1) -> (_593 : (etype A2) -> (_592 : (etype A3) -> (_591 : (etype A4) -> (_590 : (etype A5) -> (etype B) ) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (x5 : (etype A5) -> (y5 : (etype A5) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (y : (etype A1) -> (_599 : (eprop ( ( (eq A1) x1) y) ) -> (_598 : (eprop ( ( (eq A2) x2) y2) ) -> (_597 : (eprop ( ( (eq A3) x3) y3) ) -> (_596 : (eprop ( ( (eq A4) x4) y4) ) -> (_595 : (eprop ( ( (eq A5) x5) y5) ) -> (eprop ( ( (eq B) ( ( ( ( (f x1) x2) x3) x4) x5) ) ( ( ( ( (f y) y2) y3) y4) y5) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_28 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (A5 : Utype -> (B : Utype -> (f : (_609 : (etype A1) -> (_608 : (etype A2) -> (_607 : (etype A3) -> (_606 : (etype A4) -> (_605 : (etype A5) -> (etype B) ) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (x5 : (etype A5) -> (y5 : (etype A5) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (eprop ( ( (eq A1) x1) x1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, A5 : Utype, B : Utype, f : (_614 : (etype A1) -> (_613 : (etype A2) -> (_612 : (etype A3) -> (_611 : (etype A4) -> (_610 : (etype A5) -> (etype B) ) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , x5 : (etype A5) , y5 : (etype A5) , H : (eprop ( ( (eq A1) x1) y1) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_28 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) --> ( (refl_equal A1) x1) .
case_29 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (A5 : Utype -> (B : Utype -> (f : (_619 : (etype A1) -> (_618 : (etype A2) -> (_617 : (etype A3) -> (_616 : (etype A4) -> (_615 : (etype A5) -> (etype B) ) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (x5 : (etype A5) -> (y5 : (etype A5) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (y : (etype A2) -> (_623 : (eprop ( ( (eq A2) x2) y) ) -> (_622 : (eprop ( ( (eq A3) x3) y3) ) -> (_621 : (eprop ( ( (eq A4) x4) y4) ) -> (_620 : (eprop ( ( (eq A5) x5) y5) ) -> (eprop ( ( (eq B) ( ( ( ( (f x1) x2) x3) x4) x5) ) ( ( ( ( (f x1) y) y3) y4) y5) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_29 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (A5 : Utype -> (B : Utype -> (f : (_633 : (etype A1) -> (_632 : (etype A2) -> (_631 : (etype A3) -> (_630 : (etype A4) -> (_629 : (etype A5) -> (etype B) ) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (x5 : (etype A5) -> (y5 : (etype A5) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (eprop ( ( (eq A2) x2) x2) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, A5 : Utype, B : Utype, f : (_638 : (etype A1) -> (_637 : (etype A2) -> (_636 : (etype A3) -> (_635 : (etype A4) -> (_634 : (etype A5) -> (etype B) ) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , x5 : (etype A5) , y5 : (etype A5) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_29 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) --> ( (refl_equal A2) x2) .
case_30 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (A5 : Utype -> (B : Utype -> (f : (_643 : (etype A1) -> (_642 : (etype A2) -> (_641 : (etype A3) -> (_640 : (etype A4) -> (_639 : (etype A5) -> (etype B) ) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (x5 : (etype A5) -> (y5 : (etype A5) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) -> (y : (etype A3) -> (_646 : (eprop ( ( (eq A3) x3) y) ) -> (_645 : (eprop ( ( (eq A4) x4) y4) ) -> (_644 : (eprop ( ( (eq A5) x5) y5) ) -> (eprop ( ( (eq B) ( ( ( ( (f x1) x2) x3) x4) x5) ) ( ( ( ( (f x1) x2) y) y4) y5) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_30 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (A5 : Utype -> (B : Utype -> (f : (_656 : (etype A1) -> (_655 : (etype A2) -> (_654 : (etype A3) -> (_653 : (etype A4) -> (_652 : (etype A5) -> (etype B) ) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (x5 : (etype A5) -> (y5 : (etype A5) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) -> (eprop ( ( (eq A3) x3) x3) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, A5 : Utype, B : Utype, f : (_661 : (etype A1) -> (_660 : (etype A2) -> (_659 : (etype A3) -> (_658 : (etype A4) -> (_657 : (etype A5) -> (etype B) ) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , x5 : (etype A5) , y5 : (etype A5) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) , H欧1 : (eprop ( ( (eq A3) x3) y3) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_30 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) H欧1) --> ( (refl_equal A3) x3) .
case_31 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (A5 : Utype -> (B : Utype -> (f : (_666 : (etype A1) -> (_665 : (etype A2) -> (_664 : (etype A3) -> (_663 : (etype A4) -> (_662 : (etype A5) -> (etype B) ) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (x5 : (etype A5) -> (y5 : (etype A5) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) -> (H欧2 : (eprop ( ( (eq A4) x4) y4) ) -> (y : (etype A4) -> (_668 : (eprop ( ( (eq A4) x4) y) ) -> (_667 : (eprop ( ( (eq A5) x5) y5) ) -> (eprop ( ( (eq B) ( ( ( ( (f x1) x2) x3) x4) x5) ) ( ( ( ( (f x1) x2) x3) y) y5) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_31 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (A5 : Utype -> (B : Utype -> (f : (_678 : (etype A1) -> (_677 : (etype A2) -> (_676 : (etype A3) -> (_675 : (etype A4) -> (_674 : (etype A5) -> (etype B) ) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (x5 : (etype A5) -> (y5 : (etype A5) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) -> (H欧2 : (eprop ( ( (eq A4) x4) y4) ) -> (eprop ( ( (eq A4) x4) x4) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, A5 : Utype, B : Utype, f : (_683 : (etype A1) -> (_682 : (etype A2) -> (_681 : (etype A3) -> (_680 : (etype A4) -> (_679 : (etype A5) -> (etype B) ) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , x5 : (etype A5) , y5 : (etype A5) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) , H欧1 : (eprop ( ( (eq A3) x3) y3) ) , H欧2 : (eprop ( ( (eq A4) x4) y4) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_31 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) H欧1) H欧2) --> ( (refl_equal A4) x4) .
case_32 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (A5 : Utype -> (B : Utype -> (f : (_688 : (etype A1) -> (_687 : (etype A2) -> (_686 : (etype A3) -> (_685 : (etype A4) -> (_684 : (etype A5) -> (etype B) ) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (x5 : (etype A5) -> (y5 : (etype A5) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) -> (H欧2 : (eprop ( ( (eq A4) x4) y4) ) -> (H欧3 : (eprop ( ( (eq A5) x5) y5) ) -> (y : (etype A5) -> (_689 : (eprop ( ( (eq A5) x5) y) ) -> (eprop ( ( (eq B) ( ( ( ( (f x1) x2) x3) x4) x5) ) ( ( ( ( (f x1) x2) x3) x4) y) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
refl_equal_case_32 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (A5 : Utype -> (B : Utype -> (f : (_699 : (etype A1) -> (_698 : (etype A2) -> (_697 : (etype A3) -> (_696 : (etype A4) -> (_695 : (etype A5) -> (etype B) ) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (x5 : (etype A5) -> (y5 : (etype A5) -> (H : (eprop ( ( (eq A1) x1) y1) ) -> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) -> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) -> (H欧2 : (eprop ( ( (eq A4) x4) y4) ) -> (H欧3 : (eprop ( ( (eq A5) x5) y5) ) -> (eprop ( ( (eq A5) x5) x5) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, A5 : Utype, B : Utype, f : (_704 : (etype A1) -> (_703 : (etype A2) -> (_702 : (etype A3) -> (_701 : (etype A4) -> (_700 : (etype A5) -> (etype B) ) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , x5 : (etype A5) , y5 : (etype A5) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) , H欧1 : (eprop ( ( (eq A3) x3) y3) ) , H欧2 : (eprop ( ( (eq A4) x4) y4) ) , H欧3 : (eprop ( ( (eq A5) x5) y5) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_32 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) H欧1) H欧2) H欧3) --> ( (refl_equal A5) x5) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, A5 : Utype, B : Utype, f : (_694 : (etype A1) -> (_693 : (etype A2) -> (_692 : (etype A3) -> (_691 : (etype A4) -> (_690 : (etype A5) -> (etype B) ) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , x5 : (etype A5) , y5 : (etype A5) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) , H欧1 : (eprop ( ( (eq A3) x3) y3) ) , H欧2 : (eprop ( ( (eq A4) x4) y4) ) , H欧3 : (eprop ( ( (eq A5) x5) y5) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_32 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) H欧1) H欧2) H欧3) x5) ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_32 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) H欧1) H欧2) H欧3) ) --> ( (refl_equal B) ( ( ( ( (f x1) x2) x3) x4) x5) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, A5 : Utype, B : Utype, f : (_673 : (etype A1) -> (_672 : (etype A2) -> (_671 : (etype A3) -> (_670 : (etype A4) -> (_669 : (etype A5) -> (etype B) ) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , x5 : (etype A5) , y5 : (etype A5) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) , H欧1 : (eprop ( ( (eq A3) x3) y3) ) , H欧2 : (eprop ( ( (eq A4) x4) y4) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_31 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) H欧1) H欧2) x4) ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_31 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) H欧1) H欧2) ) --> (H欧3 : (eprop ( ( (eq A5) x5) y5) ) => ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_32 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) H欧1) H欧2) H欧3) y5) H欧3) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, A5 : Utype, B : Utype, f : (_651 : (etype A1) -> (_650 : (etype A2) -> (_649 : (etype A3) -> (_648 : (etype A4) -> (_647 : (etype A5) -> (etype B) ) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , x5 : (etype A5) , y5 : (etype A5) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) , H欧1 : (eprop ( ( (eq A3) x3) y3) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_30 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) H欧1) x3) ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_30 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) H欧1) ) --> (H欧2 : (eprop ( ( (eq A4) x4) y4) ) => ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_31 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) H欧1) H欧2) y4) H欧2) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, A5 : Utype, B : Utype, f : (_628 : (etype A1) -> (_627 : (etype A2) -> (_626 : (etype A3) -> (_625 : (etype A4) -> (_624 : (etype A5) -> (etype B) ) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , x5 : (etype A5) , y5 : (etype A5) , H : (eprop ( ( (eq A1) x1) y1) ) , H欧0 : (eprop ( ( (eq A2) x2) y2) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_29 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) x2) ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_29 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) ) --> (H欧1 : (eprop ( ( (eq A3) x3) y3) ) => ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_30 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) H欧1) y3) H欧1) ) .
[A1 : Utype, A2 : Utype, A3 : Utype, A4 : Utype, A5 : Utype, B : Utype, f : (_604 : (etype A1) -> (_603 : (etype A2) -> (_602 : (etype A3) -> (_601 : (etype A4) -> (_600 : (etype A5) -> (etype B) ) ) ) ) ) , x1 : (etype A1) , y1 : (etype A1) , x2 : (etype A2) , y2 : (etype A2) , x3 : (etype A3) , y3 : (etype A3) , x4 : (etype A4) , y4 : (etype A4) , x5 : (etype A5) , y5 : (etype A5) , H : (eprop ( ( (eq A1) x1) y1) ) ] ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_28 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) x1) ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (refl_equal_case_28 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) ) --> (H欧0 : (eprop ( ( (eq A2) x2) y2) ) => ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_29 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) H欧0) y2) H欧0) ) .
f_equal5 : (A1 : Utype -> (A2 : Utype -> (A3 : Utype -> (A4 : Utype -> (A5 : Utype -> (B : Utype -> (f : (_714 : (etype A1) -> (_713 : (etype A2) -> (_712 : (etype A3) -> (_711 : (etype A4) -> (_710 : (etype A5) -> (etype B) ) ) ) ) ) -> (x1 : (etype A1) -> (y1 : (etype A1) -> (x2 : (etype A2) -> (y2 : (etype A2) -> (x3 : (etype A3) -> (y3 : (etype A3) -> (x4 : (etype A4) -> (y4 : (etype A4) -> (x5 : (etype A5) -> (y5 : (etype A5) -> (_719 : (eprop ( ( (eq A1) x1) y1) ) -> (_718 : (eprop ( ( (eq A2) x2) y2) ) -> (_717 : (eprop ( ( (eq A3) x3) y3) ) -> (_716 : (eprop ( ( (eq A4) x4) y4) ) -> (_715 : (eprop ( ( (eq A5) x5) y5) ) -> (eprop ( ( (eq B) ( ( ( ( (f x1) x2) x3) x4) x5) ) ( ( ( ( (f y1) y2) y3) y4) y5) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
[] f_equal5 --> (A1 : (etype dottype) => (A2 : (etype dottype) => (A3 : (etype dottype) => (A4 : (etype dottype) => (A5 : (etype dottype) => (B : (etype dottype) => (f : (etype ( (dotpitt A1) (_709 : (etype A1) => ( (dotpitt A2) (_708 : (etype A2) => ( (dotpitt A3) (_707 : (etype A3) => ( (dotpitt A4) (_706 : (etype A4) => ( (dotpitt A5) (_705 : (etype A5) => B) ) ) ) ) ) ) ) ) ) ) => (x1 : (etype A1) => (y1 : (etype A1) => (x2 : (etype A2) => (y2 : (etype A2) => (x3 : (etype A3) => (y3 : (etype A3) => (x4 : (etype A4) => (y4 : (etype A4) => (x5 : (etype A5) => (y5 : (etype A5) => (H : (eprop ( ( (eq A1) x1) y1) ) => ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (case_28 A1) A2) A3) A4) A5) B) f) x1) y1) x2) y2) x3) y3) x4) y4) x5) y5) H) y1) H) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) .
subrelation : (A : Utype -> (B : Utype -> (R : (_726 : (etype A) -> (_725 : (etype B) -> Uprop) ) -> (R' : (_728 : (etype A) -> (_727 : (etype B) -> Uprop) ) -> Uprop) ) ) ) .
[] subrelation --> (A : (etype dottype) => (B : (etype dottype) => (R : (etype ( (dotpitt A) (_724 : (etype A) => ( (dotpitt B) (_723 : (etype B) => dotprop) ) ) ) ) => (R' : (etype ( (dotpitt A) (_722 : (etype A) => ( (dotpitt B) (_721 : (etype B) => dotprop) ) ) ) ) => ( (dotpitp A) (x : (etype A) => ( (dotpitp B) (y : (etype B) => ( (dotpipp ( (R x) y) ) (_720 : (eprop ( (R x) y) ) => ( (R' x) y) ) ) ) ) ) ) ) ) ) ) .
unique : (A : Utype -> (P : (_731 : (etype A) -> Uprop) -> (x : (etype A) -> Uprop) ) ) .
[] unique --> (A : (etype dottype) => (P : (etype ( (dotpitt A) (_730 : (etype A) => dotprop) ) ) => (x : (etype A) => ( (and (P x) ) ( (dotpitp A) (x' : (etype A) => ( (dotpipp (P x') ) (_729 : (eprop (P x') ) => ( ( (eq A) x) x') ) ) ) ) ) ) ) ) .
uniqueness : (A : Utype -> (P : (_735 : (etype A) -> Uprop) -> Uprop) ) .
[] uniqueness --> (A : (etype dottype) => (P : (etype ( (dotpitt A) (_734 : (etype A) => dotprop) ) ) => ( (dotpitp A) (x : (etype A) => ( (dotpitp A) (y : (etype A) => ( (dotpipp (P x) ) (_733 : (eprop (P x) ) => ( (dotpipp (P y) ) (_732 : (eprop (P y) ) => ( ( (eq A) x) y) ) ) ) ) ) ) ) ) ) ) .
case_33 : (A : Utype -> (P : (_738 : (etype A) -> Uprop) -> (H : (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) -> (_739 : (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) -> (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) ) ) ) ) .
conj_case_33 : (A : Utype -> (P : (_741 : (etype A) -> Uprop) -> (H : (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) -> (_743 : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) -> (_742 : (eprop ( (uniqueness A) P) ) -> (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) ) ) ) ) ) .
[A : Utype, P : (_744 : (etype A) -> Uprop) , H : (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) ] ( ( (conj_case_33 A) P) H) --> ( (conj ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) .
case_34 : (A : Utype -> (P : (_745 : (etype A) -> Uprop) -> (H : (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) -> (H欧0 : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) -> (_747 : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) -> (_746 : (eprop ( (uniqueness A) P) ) -> (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) ) ) ) ) ) ) .
ex_intro_case_34 : (A : Utype -> (P : (_749 : (etype A) -> Uprop) -> (H : (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) -> (H欧0 : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) -> (x : (etype A) -> (_750 : (eprop ( (x欧0 : (etype A) => (P x欧0) ) x) ) -> (eprop ( (ex A) (x欧0 : (etype A) => (P x欧0) ) ) ) ) ) ) ) ) ) .
[A : Utype, P : (_751 : (etype A) -> Uprop) , H : (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) , H欧0 : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) ] ( ( ( (ex_intro_case_34 A) P) H) H欧0) --> ( (ex_intro A) (x : (etype A) => (P x) ) ) .
[A : Utype, P : (_748 : (etype A) -> Uprop) , H : (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) , H欧0 : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) , var_25 : (etype A) , var_26 : (eprop ( (x : (etype A) => (P x) ) var_25) ) ] ( ( ( ( (case_34 A) P) H) H欧0) ( ( ( ( ( (ex_intro_case_34 A) P) H) H欧0) var_25) var_26) ) --> ( ( (x : (etype A) => (Hx : (eprop (P x) ) => (Huni : (eprop ( (uniqueness A) P) ) => ( ( ( (ex_intro A) ( (unique A) (x欧0 : (etype A) => (P x欧0) ) ) ) x) ( ( ( (conj (P x) ) ( (dotpitp A) (x' : (etype A) => ( (dotpipp (P x') ) (_752 : (eprop (P x') ) => ( ( (eq A) x) x') ) ) ) ) ) Hx) (x' : (etype A) => (H欧1 : (eprop (P x') ) => ( ( ( (Huni x) x') Hx) H欧1) ) ) ) ) ) ) ) var_25) var_26) .
[A : Utype, P : (_740 : (etype A) -> Uprop) , H : (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) , var_23 : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) , var_24 : (eprop ( (uniqueness A) P) ) ] ( ( ( (case_33 A) P) H) ( ( ( ( (conj_case_33 A) P) H) var_23) var_24) ) --> ( ( (H欧0 : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) => ( ( ( ( (case_34 A) P) H) H欧0) H欧0) ) var_23) var_24) .
case_35 : (A : Utype -> (P : (_753 : (etype A) -> Uprop) -> (H : (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) -> (_754 : (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) -> (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) ) ) ) ) .
ex_intro_case_35 : (A : Utype -> (P : (_756 : (etype A) -> Uprop) -> (H : (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) -> (x : (etype A) -> (_757 : (eprop ( ( (unique A) (x欧0 : (etype A) => (P x欧0) ) ) x) ) -> (eprop ( (ex A) ( (unique A) (x欧0 : (etype A) => (P x欧0) ) ) ) ) ) ) ) ) ) .
[A : Utype, P : (_758 : (etype A) -> Uprop) , H : (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) ] ( ( (ex_intro_case_35 A) P) H) --> ( (ex_intro A) ( (unique A) (x : (etype A) => (P x) ) ) ) .
case_36 : (A : Utype -> (P : (_759 : (etype A) -> Uprop) -> (H : (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) -> (x : (etype A) -> (H欧0 : (eprop ( ( (unique A) (x欧0 : (etype A) => (P x欧0) ) ) x) ) -> (_761 : (eprop ( (and (P x) ) ( (dotpitp A) (x' : (etype A) => ( (dotpipp (P x') ) (_760 : (eprop (P x') ) => ( ( (eq A) x) x') ) ) ) ) ) ) -> (eprop ( (and ( (ex A) (x欧0 : (etype A) => (P x欧0) ) ) ) ( (uniqueness A) P) ) ) ) ) ) ) ) ) .
conj_case_36 : (A : Utype -> (P : (_764 : (etype A) -> Uprop) -> (H : (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) -> (x : (etype A) -> (H欧0 : (eprop ( ( (unique A) (x欧0 : (etype A) => (P x欧0) ) ) x) ) -> (_768 : (eprop (P x) ) -> (_767 : (x' : (etype A) -> (_765 : (eprop (P x') ) -> (eprop ( ( (eq A) x) x') ) ) ) -> (eprop ( (and (P x) ) ( (dotpitp A) (x' : (etype A) => ( (dotpipp (P x') ) (_766 : (eprop (P x') ) => ( ( (eq A) x) x') ) ) ) ) ) ) ) ) ) ) ) ) ) .
[A : Utype, P : (_769 : (etype A) -> Uprop) , H : (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) , x : (etype A) , H欧0 : (eprop ( ( (unique A) (x欧0 : (etype A) => (P x欧0) ) ) x) ) ] ( ( ( ( (conj_case_36 A) P) H) x) H欧0) --> ( (conj (P x) ) ( (dotpitp A) (x' : (etype A) => ( (dotpipp (P x') ) (_763 : (eprop (P x') ) => ( ( (eq A) x) x') ) ) ) ) ) .
[A : Utype, P : (_762 : (etype A) -> Uprop) , H : (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) , x : (etype A) , H欧0 : (eprop ( ( (unique A) (x欧0 : (etype A) => (P x欧0) ) ) x) ) , var_29 : (eprop (P x) ) , var_30 : (x' : (etype A) -> (_770 : (eprop (P x') ) -> (eprop ( ( (eq A) x) x') ) ) ) ] ( ( ( ( ( (case_36 A) P) H) x) H欧0) ( ( ( ( ( ( (conj_case_36 A) P) H) x) H欧0) var_29) var_30) ) --> ( ( (Hx : (eprop (P x) ) => (Huni : (eprop ( (dotpitp A) (x' : (etype A) => ( (dotpipp (P x') ) (_771 : (eprop (P x') ) => ( ( (eq A) x) x') ) ) ) ) ) => ( ( ( (conj ( (ex A) (x欧0 : (etype A) => (P x欧0) ) ) ) ( (uniqueness A) P) ) ( ( ( (ex_intro A) (x欧0 : (etype A) => (P x欧0) ) ) x) Hx) ) (x' : (etype A) => (x'' : (etype A) => (Hx' : (eprop (P x') ) => (Hx'' : (eprop (P x'') ) => ( ( ( ( ( (trans_eq A) x') x) x'') ( ( ( (sym_eq A) x) x') ( (Huni x') Hx') ) ) ( (Huni x'') Hx'') ) ) ) ) ) ) ) ) var_29) var_30) .
[A : Utype, P : (_755 : (etype A) -> Uprop) , H : (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) , var_27 : (etype A) , var_28 : (eprop ( ( (unique A) (x : (etype A) => (P x) ) ) var_27) ) ] ( ( ( (case_35 A) P) H) ( ( ( ( (ex_intro_case_35 A) P) H) var_27) var_28) ) --> ( ( (x : (etype A) => (H欧0 : (eprop ( ( (unique A) (x欧0 : (etype A) => (P x欧0) ) ) x) ) => ( ( ( ( ( (case_36 A) P) H) x) H欧0) H欧0) ) ) var_27) var_28) .
unique_existence : (A : Utype -> (P : (_773 : (etype A) -> Uprop) -> (eprop ( (iff ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) ) ) ) .
[] unique_existence --> (A : (etype dottype) => (P : (etype ( (dotpitt A) (_772 : (etype A) => dotprop) ) ) => ( ( ( (conj ( (dotpipp ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) (_736 : (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) => ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) ) ) ( (dotpipp ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) (_737 : (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) => ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) ) ) (H : (eprop ( (and ( (ex A) (x : (etype A) => (P x) ) ) ) ( (uniqueness A) P) ) ) => ( ( ( (case_33 A) P) H) H) ) ) (H : (eprop ( (ex A) ( (unique A) (x : (etype A) => (P x) ) ) ) ) => ( ( ( (case_35 A) P) H) H) ) ) ) ) .
inhabited : (A : Utype -> Uprop) .
inhabits : (A : Utype -> (_774 : (etype A) -> (eprop (inhabited A) ) ) ) .
case_37 : (A : Utype -> (P : Uprop -> (f : (_775 : (etype A) -> (eprop P) ) -> (i : (eprop (inhabited A) ) -> (_776 : (eprop (inhabited A) ) -> (eprop P) ) ) ) ) ) .
inhabits_case_37 : (A : Utype -> (P : Uprop -> (f : (_778 : (etype A) -> (eprop P) ) -> (i : (eprop (inhabited A) ) -> (_779 : (etype A) -> (eprop (inhabited A) ) ) ) ) ) ) .
[A : Utype, P : Uprop, f : (_780 : (etype A) -> (eprop P) ) , i : (eprop (inhabited A) ) ] ( ( ( (inhabits_case_37 A) P) f) i) --> (inhabits A) .
[A : Utype, P : Uprop, f : (_777 : (etype A) -> (eprop P) ) , i : (eprop (inhabited A) ) , var_31 : (etype A) ] ( ( ( ( (case_37 A) P) f) i) ( ( ( ( (inhabits_case_37 A) P) f) i) var_31) ) --> (f var_31) .
inhabited_ind : (A : Utype -> (P : Uprop -> (f : (_782 : (etype A) -> (eprop P) ) -> (i : (eprop (inhabited A) ) -> (eprop P) ) ) ) ) .
[] inhabited_ind --> (A : (etype dottype) => (P : (etype dotprop) => (f : (eprop ( (dotpitp A) (_781 : (etype A) => P) ) ) => (i : (eprop (inhabited A) ) => ( ( ( ( (case_37 A) P) f) i) i) ) ) ) ) .
case_38 : (A : Utype -> (P : (_783 : (etype A) -> Uprop) -> (H : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) -> (_784 : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) -> (eprop (inhabited A) ) ) ) ) ) .
ex_intro_case_38 : (A : Utype -> (P : (_786 : (etype A) -> Uprop) -> (H : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) -> (x : (etype A) -> (_787 : (eprop ( (x欧0 : (etype A) => (P x欧0) ) x) ) -> (eprop ( (ex A) (x欧0 : (etype A) => (P x欧0) ) ) ) ) ) ) ) ) .
[A : Utype, P : (_788 : (etype A) -> Uprop) , H : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) ] ( ( (ex_intro_case_38 A) P) H) --> ( (ex_intro A) (x : (etype A) => (P x) ) ) .
[A : Utype, P : (_785 : (etype A) -> Uprop) , H : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) , var_32 : (etype A) , var_33 : (eprop ( (x : (etype A) => (P x) ) var_32) ) ] ( ( ( (case_38 A) P) H) ( ( ( ( (ex_intro_case_38 A) P) H) var_32) var_33) ) --> ( ( (x : (etype A) => (H欧0 : (eprop (P x) ) => ( (inhabits A) x) ) ) var_32) var_33) .
exists_inhabited : (A : Utype -> (P : (_790 : (etype A) -> Uprop) -> (_791 : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) -> (eprop (inhabited A) ) ) ) ) .
[] exists_inhabited --> (A : (etype dottype) => (P : (etype ( (dotpitt A) (_789 : (etype A) => dotprop) ) ) => (H : (eprop ( (ex A) (x : (etype A) => (P x) ) ) ) => ( ( ( (case_38 A) P) H) H) ) ) ) .
eq_stepl : (A : Utype -> (x : (etype A) -> (y : (etype A) -> (z : (etype A) -> (_793 : (eprop ( ( (eq A) x) y) ) -> (_792 : (eprop ( ( (eq A) x) z) ) -> (eprop ( ( (eq A) z) y) ) ) ) ) ) ) ) .
[] eq_stepl --> (A : (etype dottype) => (x : (etype A) => (y : (etype A) => (z : (etype A) => (H1 : (eprop ( ( (eq A) x) y) ) => (H2 : (eprop ( ( (eq A) x) z) ) => ( ( ( ( ( (eq_ind A) x) (z欧0 : (etype A) => ( ( (eq A) z欧0) y) ) ) H1) z) H2) ) ) ) ) ) ) .
iff_stepl : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_805 : (eprop ( (iff A) B) ) -> (_804 : (eprop ( (iff A) C) ) -> (eprop ( (iff C) B) ) ) ) ) ) ) .
[] iff_stepl --> (A : (etype dotprop) => (B : (etype dotprop) => (C : (etype dotprop) => (H : (eprop ( (iff A) B) ) => (H0 : (eprop ( (iff A) C) ) => ( ( ( ( (and_ind ( (dotpipp A) (_794 : (eprop A) => B) ) ) ( (dotpipp B) (_795 : (eprop B) => A) ) ) ( (iff C) B) ) (H1 : (eprop ( (dotpipp A) (_803 : (eprop A) => B) ) ) => (H2 : (eprop ( (dotpipp B) (_802 : (eprop B) => A) ) ) => ( ( ( ( (and_ind ( (dotpipp A) (_796 : (eprop A) => C) ) ) ( (dotpipp C) (_797 : (eprop C) => A) ) ) ( (iff C) B) ) (H欧0 : (eprop ( (dotpipp A) (_801 : (eprop A) => C) ) ) => (H3 : (eprop ( (dotpipp C) (_800 : (eprop C) => A) ) ) => ( ( ( (conj ( (dotpipp C) (_798 : (eprop C) => B) ) ) ( (dotpipp B) (_799 : (eprop B) => C) ) ) (H0欧0 : (eprop C) => ( (H4 : (eprop A) => ( (H3欧0 : (eprop B) => ( (H1欧0 : (eprop C) => ( (H欧1 : (eprop A) => H3欧0) (H2 H3欧0) ) ) (H欧0 H4) ) ) (H1 H4) ) ) (H3 H0欧0) ) ) ) (H0欧0 : (eprop B) => ( (H4 : (eprop A) => ( (H2欧0 : (eprop B) => ( (H1欧0 : (eprop C) => ( (H欧1 : (eprop A) => H1欧0) (H3 H1欧0) ) ) (H欧0 H4) ) ) (H1 H4) ) ) (H2 H0欧0) ) ) ) ) ) ) H0) ) ) ) H) ) ) ) ) ) .
;Finished module Logic