dedukti-1.0.0: t/Logicavecprelude.eu
Uset : Type.
Uprop : Type.
Utype : Type.
eprop : x : Uprop -> Type.
eset : x : Uset -> Type.
etype : x : Utype -> Type.
dotset : Utype.
dotprop : Utype.
; /!\ type : type /!\, should use universes
dottype : Utype.
; /!\ subtyping in coq, should be unidirectional /!\
[] Uprop --> Utype.
[] Uset --> Utype.
dotpipp : x : Uprop -> y : (eprop x -> Uprop) -> Uprop.
dotpips : x : Uprop -> y : (eprop x -> Uset) -> Uset.
dotpipt : x : Uprop -> y : (eprop x -> Utype) -> Utype.
dotpisp : x : Uset -> y : (eset x -> Uprop) -> Uprop.
dotpitp : x : Utype -> y : (etype x -> Uprop) -> Uprop.
dotpist : x : Uset -> y : (eset x -> Utype) -> Utype.
dotpits : x : Utype -> y : (etype x -> Uset) -> Uset.
dotpiss : x : Uset -> y : (eset x -> Uset) -> Uset.
dotpitt : x : Utype -> y : (etype x -> Utype) -> Utype.
[x:Uprop, y : eprop x -> Uprop]
eprop (dotpipp x y) --> w : eprop x -> eprop (y w).
[x:Uset, y : eset x -> Uprop]
eprop (dotpisp x y) --> w : eset x -> eprop (y w).
[x:Utype, y : etype x -> Uprop]
eprop (dotpitp x y) --> w : etype x -> eprop (y w).
; /!\
[P : Uprop] eprop P --> etype P.
[x:Uprop, y : eprop x -> Uset]
eset (dotpips x y) --> w : eprop x -> eset (y w).
[x:Utype, y : etype x -> Uset]
eset (dotpits x y) --> w : etype x -> eset (y w).
[x:Uset, y : eset x -> Uset]
eset (dotpiss x y) --> w : eset x -> eset (y w).
; /!\
[P : Uset] eset P --> etype P.
[x:Uset, y : eset x -> Utype]
etype (dotpist x y) --> w : eset x -> etype (y w).
[x:Utype, y : etype x -> Utype]
etype (dotpitt x y) --> w : etype x -> etype (y w).
[x:Uprop, y : eprop x -> Utype]
etype (dotpipt x y) --> w : eprop x -> etype (y w).
[] (etype dotset) --> Uset.
[] (etype dotprop) --> Uprop.
; /!\
[] (etype dottype) --> Utype.
; end of Coq1univ
True : Uprop.
I : (eprop True) .
case_0 : (P : Utype -> (f : (etype P) -> (t : (eprop True) -> (_0 : (eprop True) -> (etype P) ) ) ) ) .
[P : Utype, f : (etype P) , t : (eprop True) ] ( ( ( (case_0 P) f) t) I) --> 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) ) ) ) ) ) ) .
[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 A) B) var_0) var_1) ) --> ( (f var_0) var_1) .
and_rect : (A : Uprop -> (B : Uprop -> (P : Utype -> (f : (_13 : (eprop A) -> (_12 : (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) (_11 : (eprop A) => ( (dotpipt B) (_10 : (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 : (_15 : (eprop A) -> (_14 : (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 : (_17 : (eprop A) -> (_16 : (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) ) -> (_18 : (eprop ( (and A) B) ) -> (eprop A) ) ) ) ) .
[A : Uprop, B : Uprop, H : (eprop ( (and A) B) ) , var_2 : (eprop A) , var_3 : (eprop B) ] ( ( ( (case_3 A) B) H) ( ( ( (conj A) B) var_2) var_3) ) --> ( ( (H0 : (eprop A) => (H0 : (eprop B) => H0) ) var_2) var_3) .
proj1 : (A : Uprop -> (B : Uprop -> (_19 : (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) ) -> (_20 : (eprop ( (and A) B) ) -> (eprop B) ) ) ) ) .
[A : Uprop, B : Uprop, H : (eprop ( (and A) B) ) , var_4 : (eprop A) , var_5 : (eprop B) ] ( ( ( (case_4 A) B) H) ( ( ( (conj A) B) var_4) var_5) ) --> ( ( (H0 : (eprop A) => (H0 : (eprop B) => H0) ) var_4) var_5) .
proj2 : (A : Uprop -> (B : Uprop -> (_21 : (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 -> (_22 : (eprop A) -> (eprop ( (or A) B) ) ) ) ) .
or_intror : (A : Uprop -> (B : Uprop -> (_23 : (eprop B) -> (eprop ( (or A) B) ) ) ) ) .
case_5 : (A : Uprop -> (B : Uprop -> (P : Uprop -> (f : (_24 : (eprop A) -> (eprop P) ) -> (f0 : (_25 : (eprop B) -> (eprop P) ) -> (o : (eprop ( (or A) B) ) -> (_26 : (eprop ( (or A) B) ) -> (eprop P) ) ) ) ) ) ) ) .
[A : Uprop, B : Uprop, P : Uprop, f : (_27 : (eprop A) -> (eprop P) ) , f0 : (_28 : (eprop B) -> (eprop P) ) , o : (eprop ( (or A) B) ) , var_6 : (eprop A) ] ( ( ( ( ( ( (case_5 A) B) P) f) f0) o) ( ( (or_introl A) B) var_6) ) --> (f var_6) .
[A : Uprop, B : Uprop, P : Uprop, f : (_27 : (eprop A) -> (eprop P) ) , f0 : (_28 : (eprop B) -> (eprop P) ) , o : (eprop ( (or A) B) ) , var_7 : (eprop B) ] ( ( ( ( ( ( (case_5 A) B) P) f) f0) o) ( ( (or_intror A) B) var_7) ) --> (f0 var_7) .
or_ind : (A : Uprop -> (B : Uprop -> (P : Uprop -> (f : (_31 : (eprop A) -> (eprop P) ) -> (f0 : (_32 : (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) (_30 : (eprop A) => P) ) ) => (f0 : (eprop ( (dotpipp B) (_29 : (eprop B) => P) ) ) => (o : (eprop ( (or A) B) ) => ( ( ( ( ( ( (case_5 A) B) P) f) f0) o) o) ) ) ) ) ) ) .
iff : (A : Uprop -> (B : Uprop -> Uprop) ) .
[] iff --> (A : (etype dotprop) => (B : (etype dotprop) => ( (and ( (dotpipp A) (_33 : (eprop A) => B) ) ) ( (dotpipp B) (_34 : (eprop B) => A) ) ) ) ) .
iff_refl : (A : Uprop -> (eprop ( (iff A) A) ) ) .
[] iff_refl --> (A : (etype dotprop) => ( ( ( (conj ( (dotpipp A) (_35 : (eprop A) => A) ) ) ( (dotpipp A) (_36 : (eprop A) => A) ) ) (H : (eprop A) => H) ) (H : (eprop A) => H) ) ) .
case_6 : (A : Uprop -> (B : Uprop -> (C : Uprop -> (H : (eprop ( (iff A) B) ) -> (_40 : (eprop ( (and ( (dotpipp A) (_37 : (eprop A) => B) ) ) ( (dotpipp B) (_38 : (eprop B) => A) ) ) ) -> (_39 : (eprop ( (iff B) C) ) -> (eprop ( (iff A) C) ) ) ) ) ) ) ) .
case_7 : (A : Uprop -> (B : Uprop -> (C : Uprop -> (H : (eprop ( (iff A) B) ) -> (H1 : (_41 : (eprop A) -> (eprop B) ) -> (H2 : (_42 : (eprop B) -> (eprop A) ) -> (H0 : (eprop ( (iff B) C) ) -> (_45 : (eprop ( (and ( (dotpipp B) (_43 : (eprop B) => C) ) ) ( (dotpipp C) (_44 : (eprop C) => B) ) ) ) -> (eprop ( (iff A) C) ) ) ) ) ) ) ) ) ) .
[A : Uprop, B : Uprop, C : Uprop, H : (eprop ( (iff A) B) ) , H1 : (_46 : (eprop A) -> (eprop B) ) , H2 : (_47 : (eprop B) -> (eprop A) ) , H0 : (eprop ( (iff B) C) ) , var_10 : (eprop B) , var_11 : (eprop C) ] ( ( ( ( ( ( ( (case_7 A) B) C) H) H1) H2) H0) ( ( ( (conj B) C) var_10) var_11) ) --> ( ( (H3 : (eprop ( (dotpipp B) (_51 : (eprop B) => C) ) ) => (H4 : (eprop ( (dotpipp C) (_50 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp A) (_48 : (eprop A) => C) ) ) ( (dotpipp C) (_49 : (eprop C) => A) ) ) (H1 : (eprop A) => (H3 (H1 H1) ) ) ) (H1 : (eprop C) => (H2 (H1 (H2 (H4 H1) ) ) ) ) ) ) ) var_10) var_11) .
[A : Uprop, B : Uprop, C : Uprop, H : (eprop ( (iff A) B) ) , var_8 : (eprop A) , var_9 : (eprop B) ] ( ( ( ( (case_6 A) B) C) H) ( ( ( (conj A) B) var_8) var_9) ) --> ( ( (H1 : (eprop ( (dotpipp A) (_53 : (eprop A) => B) ) ) => (H2 : (eprop ( (dotpipp B) (_52 : (eprop B) => A) ) ) => (H0 : (eprop ( (iff B) C) ) => ( ( ( ( ( ( ( (case_7 A) B) C) H) H1) H2) H0) H0) ) ) ) var_8) var_9) .
iff_trans : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_55 : (eprop ( (iff A) B) ) -> (_54 : (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) ) -> (_58 : (eprop ( (and ( (dotpipp A) (_56 : (eprop A) => B) ) ) ( (dotpipp B) (_57 : (eprop B) => A) ) ) ) -> (eprop ( (iff B) A) ) ) ) ) ) .
[A : Uprop, B : Uprop, H : (eprop ( (iff A) B) ) , var_12 : (eprop A) , var_13 : (eprop B) ] ( ( ( (case_8 A) B) H) ( ( ( (conj A) B) var_12) var_13) ) --> ( ( (H1 : (eprop ( (dotpipp A) (_62 : (eprop A) => B) ) ) => (H2 : (eprop ( (dotpipp B) (_61 : (eprop B) => A) ) ) => ( ( ( (conj ( (dotpipp B) (_59 : (eprop B) => A) ) ) ( (dotpipp A) (_60 : (eprop A) => B) ) ) H2) H1) ) ) var_12) var_13) .
iff_sym : (A : Uprop -> (B : Uprop -> (_63 : (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) ) -> (_74 : (eprop ( (and ( (dotpipp A) (_71 : (eprop A) => False) ) ) ( (dotpipp False) (_72 : (eprop False) => A) ) ) ) -> (_73 : (eprop A) -> (eprop False) ) ) ) ) .
[A : Uprop, H : (eprop ( (iff A) False) ) , var_14 : (eprop A) , var_15 : (eprop False) ] ( ( (case_9 A) H) ( ( ( (conj A) False) var_14) var_15) ) --> ( ( (H0 : (eprop ( (dotpipp A) (_76 : (eprop A) => False) ) ) => (H0 : (eprop ( (dotpipp False) (_75 : (eprop False) => A) ) ) => H0) ) var_14) var_15) .
neg_false : (A : Uprop -> (eprop ( (iff (not A) ) ( (iff A) False) ) ) ) .
[] neg_false --> (A : (etype dotprop) => ( ( ( (conj ( (dotpipp ( (dotpipp A) (_64 : (eprop A) => False) ) ) (_65 : (eprop ( (dotpipp A) (_64 : (eprop A) => False) ) ) => ( (iff A) False) ) ) ) ( (dotpipp ( (iff A) False) ) (_67 : (eprop ( (iff A) False) ) => ( (dotpipp A) (_66 : (eprop A) => False) ) ) ) ) (H : (eprop ( (dotpipp A) (_70 : (eprop A) => False) ) ) => ( ( ( (conj ( (dotpipp A) (_68 : (eprop A) => False) ) ) ( (dotpipp False) (_69 : (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 -> (_104 : (_101 : (eprop B) -> (eprop A) ) -> (_103 : (_102 : (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) (_100 : (eprop B) => A) ) ) => (H0 : (eprop ( (dotpipp C) (_99 : (eprop C) => A) ) ) => ( ( ( (conj ( (dotpipp ( (iff ( (and A) B) ) ( (and A) C) ) ) (_77 : (eprop ( (iff ( (and A) B) ) ( (and A) C) ) ) => ( (iff B) C) ) ) ) ( (dotpipp ( (iff B) C) ) (_78 : (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) ) (_79 : (eprop ( (and A) B) ) => ( (and A) C) ) ) ) ( (dotpipp ( (and A) C) ) (_80 : (eprop ( (and A) C) ) => ( (and A) B) ) ) ) ( (iff B) C) ) (H2 : (eprop ( (dotpipp ( (and A) B) ) (_92 : (eprop ( (and A) B) ) => ( (and A) C) ) ) ) => (H3 : (eprop ( (dotpipp ( (and A) C) ) (_91 : (eprop ( (and A) C) ) => ( (and A) B) ) ) ) => ( (H10 : (eprop ( (dotpipp A) (_90 : (eprop A) => ( (dotpipp B) (_89 : (eprop B) => ( (and A) C) ) ) ) ) ) => ( (H20 : (eprop ( (dotpipp A) (_88 : (eprop A) => ( (dotpipp C) (_87 : (eprop C) => ( (and A) B) ) ) ) ) ) => ( ( ( (conj ( (dotpipp B) (_81 : (eprop B) => C) ) ) ( (dotpipp C) (_82 : (eprop C) => B) ) ) (H30 : (eprop B) => ( (H4 : (eprop A) => ( (H0 : (eprop ( (dotpipp B) (_84 : (eprop B) => ( (and A) C) ) ) ) => ( (H11 : (eprop ( (and A) C) ) => ( ( ( ( (and_ind A) C) C) (H1 : (eprop A) => (H5 : (eprop C) => ( (H12 : (eprop ( (dotpipp C) (_83 : (eprop C) => ( (and A) B) ) ) ) => ( (H21 : (eprop A) => ( (H00 : (eprop ( (and A) B) ) => ( ( ( ( (and_ind A) B) C) (H13 : (eprop A) => (H6 : (eprop B) => H5) ) ) H00) ) (H12 H5) ) ) (H0 H5) ) ) (H20 H4) ) ) ) ) H11) ) (H0 H30) ) ) (H10 H4) ) ) (H H30) ) ) ) (H30 : (eprop C) => ( (H4 : (eprop A) => ( (H00 : (eprop ( (dotpipp B) (_86 : (eprop B) => ( (and A) C) ) ) ) => ( (H11 : (eprop ( (dotpipp C) (_85 : (eprop C) => ( (and A) B) ) ) ) => ( (H21 : (eprop ( (and A) B) ) => ( ( ( ( (and_ind A) B) B) (H12 : (eprop A) => (H5 : (eprop B) => ( (H22 : (eprop A) => ( (H0 : (eprop ( (and A) C) ) => ( ( ( ( (and_ind A) C) B) (H01 : (eprop A) => (H6 : (eprop C) => H5) ) ) H0) ) (H00 H5) ) ) (H H5) ) ) ) ) H21) ) (H11 H30) ) ) (H20 H4) ) ) (H10 H4) ) ) (H0 H30) ) ) ) ) (H20 : (eprop A) => (H4 : (eprop C) => (H3 ( ( ( (conj A) C) H20) H4) ) ) ) ) ) (H10 : (eprop A) => (H4 : (eprop B) => (H2 ( ( ( (conj A) B) H10) H4) ) ) ) ) ) ) ) H1) ) ) (H1 : (eprop ( (iff B) C) ) => ( ( ( ( (and_ind ( (dotpipp B) (_93 : (eprop B) => C) ) ) ( (dotpipp C) (_94 : (eprop C) => B) ) ) ( (iff ( (and A) B) ) ( (and A) C) ) ) (H2 : (eprop ( (dotpipp B) (_98 : (eprop B) => C) ) ) => (H3 : (eprop ( (dotpipp C) (_97 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (and A) B) ) (_95 : (eprop ( (and A) B) ) => ( (and A) C) ) ) ) ( (dotpipp ( (and A) C) ) (_96 : (eprop ( (and A) C) ) => ( (and A) B) ) ) ) (H10 : (eprop ( (and A) B) ) => ( ( ( ( (and_ind A) B) ( (and A) C) ) (H4 : (eprop A) => (H5 : (eprop B) => ( (H11 : (eprop A) => ( (H0 : (eprop C) => ( (H20 : (eprop A) => ( (H00 : (eprop B) => ( ( ( (conj A) C) H20) H0) ) (H3 H0) ) ) (H0 H0) ) ) (H2 H5) ) ) (H H5) ) ) ) ) H10) ) ) (H10 : (eprop ( (and A) C) ) => ( ( ( ( (and_ind A) C) ( (and A) B) ) (H4 : (eprop A) => (H5 : (eprop C) => ( (H11 : (eprop A) => ( (H00 : (eprop B) => ( (H30 : (eprop A) => ( (H0 : (eprop C) => ( ( ( (conj A) B) H30) H00) ) (H2 H00) ) ) (H H00) ) ) (H3 H5) ) ) (H0 H5) ) ) ) ) H10) ) ) ) ) ) H1) ) ) ) ) ) ) ) .
and_cancel_r : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_132 : (_129 : (eprop B) -> (eprop A) ) -> (_131 : (_130 : (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) (_128 : (eprop B) => A) ) ) => (H0 : (eprop ( (dotpipp C) (_127 : (eprop C) => A) ) ) => ( ( ( (conj ( (dotpipp ( (iff ( (and B) A) ) ( (and C) A) ) ) (_105 : (eprop ( (iff ( (and B) A) ) ( (and C) A) ) ) => ( (iff B) C) ) ) ) ( (dotpipp ( (iff B) C) ) (_106 : (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) ) (_107 : (eprop ( (and B) A) ) => ( (and C) A) ) ) ) ( (dotpipp ( (and C) A) ) (_108 : (eprop ( (and C) A) ) => ( (and B) A) ) ) ) ( (iff B) C) ) (H2 : (eprop ( (dotpipp ( (and B) A) ) (_120 : (eprop ( (and B) A) ) => ( (and C) A) ) ) ) => (H3 : (eprop ( (dotpipp ( (and C) A) ) (_119 : (eprop ( (and C) A) ) => ( (and B) A) ) ) ) => ( (H10 : (eprop ( (dotpipp B) (_118 : (eprop B) => ( (dotpipp A) (_117 : (eprop A) => ( (and C) A) ) ) ) ) ) => ( (H20 : (eprop ( (dotpipp C) (_116 : (eprop C) => ( (dotpipp A) (_115 : (eprop A) => ( (and B) A) ) ) ) ) ) => ( ( ( (conj ( (dotpipp B) (_109 : (eprop B) => C) ) ) ( (dotpipp C) (_110 : (eprop C) => B) ) ) (H30 : (eprop B) => ( (H4 : (eprop A) => ( (H0 : (eprop ( (dotpipp A) (_112 : (eprop A) => ( (and C) A) ) ) ) => ( (H11 : (eprop ( (and C) A) ) => ( ( ( ( (and_ind C) A) C) (H1 : (eprop C) => (H5 : (eprop A) => ( (H12 : (eprop A) => ( (H00 : (eprop ( (dotpipp A) (_111 : (eprop A) => ( (and B) A) ) ) ) => ( (H21 : (eprop ( (and B) A) ) => ( ( ( ( (and_ind B) A) C) (H01 : (eprop B) => (H6 : (eprop A) => H1) ) ) H21) ) (H00 H4) ) ) (H20 H1) ) ) (H0 H1) ) ) ) ) H11) ) (H0 H4) ) ) (H10 H30) ) ) (H H30) ) ) ) (H30 : (eprop C) => ( (H4 : (eprop A) => ( (H00 : (eprop ( (dotpipp A) (_114 : (eprop A) => ( (and B) A) ) ) ) => ( (H21 : (eprop ( (and B) A) ) => ( ( ( ( (and_ind B) A) B) (H01 : (eprop B) => (H5 : (eprop A) => ( (H22 : (eprop A) => ( (H0 : (eprop ( (dotpipp A) (_113 : (eprop A) => ( (and C) A) ) ) ) => ( (H11 : (eprop ( (and C) A) ) => ( ( ( ( (and_ind C) A) B) (H1 : (eprop C) => (H6 : (eprop A) => H01) ) ) H11) ) (H0 H4) ) ) (H10 H01) ) ) (H H01) ) ) ) ) H21) ) (H00 H4) ) ) (H20 H30) ) ) (H0 H30) ) ) ) ) (H20 : (eprop C) => (H4 : (eprop A) => (H3 ( ( ( (conj C) A) H20) H4) ) ) ) ) ) (H10 : (eprop B) => (H4 : (eprop A) => (H2 ( ( ( (conj B) A) H10) H4) ) ) ) ) ) ) ) H1) ) ) (H1 : (eprop ( (iff B) C) ) => ( ( ( ( (and_ind ( (dotpipp B) (_121 : (eprop B) => C) ) ) ( (dotpipp C) (_122 : (eprop C) => B) ) ) ( (iff ( (and B) A) ) ( (and C) A) ) ) (H2 : (eprop ( (dotpipp B) (_126 : (eprop B) => C) ) ) => (H3 : (eprop ( (dotpipp C) (_125 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (and B) A) ) (_123 : (eprop ( (and B) A) ) => ( (and C) A) ) ) ) ( (dotpipp ( (and C) A) ) (_124 : (eprop ( (and C) A) ) => ( (and B) A) ) ) ) (H10 : (eprop ( (and B) A) ) => ( ( ( ( (and_ind B) A) ( (and C) A) ) (H4 : (eprop B) => (H5 : (eprop A) => ( (H11 : (eprop A) => ( (H0 : (eprop C) => ( (H20 : (eprop A) => ( (H00 : (eprop B) => ( ( ( (conj C) A) H0) H20) ) (H3 H0) ) ) (H0 H0) ) ) (H2 H4) ) ) (H H4) ) ) ) ) H10) ) ) (H10 : (eprop ( (and C) A) ) => ( ( ( ( (and_ind C) A) ( (and B) A) ) (H4 : (eprop C) => (H5 : (eprop A) => ( (H11 : (eprop A) => ( (H00 : (eprop B) => ( (H30 : (eprop A) => ( (H0 : (eprop C) => ( ( ( (conj B) A) H00) H30) ) (H2 H00) ) ) (H H00) ) ) (H3 H4) ) ) (H0 H4) ) ) ) ) H10) ) ) ) ) ) H1) ) ) ) ) ) ) ) .
or_cancel_l : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_156 : (_153 : (eprop B) -> (eprop (not A) ) ) -> (_155 : (_154 : (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) (_152 : (eprop B) => (not A) ) ) ) => (H0 : (eprop ( (dotpipp C) (_151 : (eprop C) => (not A) ) ) ) => ( ( ( (conj ( (dotpipp ( (iff ( (or A) B) ) ( (or A) C) ) ) (_133 : (eprop ( (iff ( (or A) B) ) ( (or A) C) ) ) => ( (iff B) C) ) ) ) ( (dotpipp ( (iff B) C) ) (_134 : (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) ) (_135 : (eprop ( (or A) B) ) => ( (or A) C) ) ) ) ( (dotpipp ( (or A) C) ) (_136 : (eprop ( (or A) C) ) => ( (or A) B) ) ) ) ( (iff B) C) ) (H2 : (eprop ( (dotpipp ( (or A) B) ) (_144 : (eprop ( (or A) B) ) => ( (or A) C) ) ) ) => (H3 : (eprop ( (dotpipp ( (or A) C) ) (_143 : (eprop ( (or A) C) ) => ( (or A) B) ) ) ) => ( (H10 : (eprop ( (dotpipp A) (_142 : (eprop A) => ( (or A) C) ) ) ) => ( (H4 : (eprop ( (dotpipp B) (_141 : (eprop B) => ( (or A) C) ) ) ) => ( (H20 : (eprop ( (dotpipp A) (_140 : (eprop A) => ( (or A) B) ) ) ) => ( (H5 : (eprop ( (dotpipp C) (_139 : (eprop C) => ( (or A) B) ) ) ) => ( ( ( (conj ( (dotpipp B) (_137 : (eprop B) => C) ) ) ( (dotpipp C) (_138 : (eprop C) => B) ) ) (H30 : (eprop B) => ( (H6 : (eprop (not A) ) => ( (H0 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) C) (H40 : (eprop A) => ( (H1 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) C) (H11 : (eprop A) => ( (H2 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H21 : (eprop A) => ( (H3 : (eprop False) => ( (False_ind C) H3) ) (H6 H40) ) ) ) (H21 : (eprop B) => ( (H3 : (eprop False) => ( (False_ind C) H3) ) (H6 H40) ) ) ) H2) ) (H20 H40) ) ) ) (H11 : (eprop C) => ( (H2 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H21 : (eprop A) => ( (H3 : (eprop False) => ( (H60 : (eprop (not A) ) => ( (H00 : (eprop False) => ( (H61 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H50 : (eprop A) => ( (False_ind C) H00) ) ) (H50 : (eprop B) => ( (False_ind C) H00) ) ) H61) ) (H5 H11) ) ) (H60 H40) ) ) (H0 H11) ) ) (H6 H40) ) ) ) (H21 : (eprop B) => ( (H3 : (eprop False) => ( (H60 : (eprop (not A) ) => ( (H00 : (eprop False) => ( (H61 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H50 : (eprop A) => ( (False_ind C) H00) ) ) (H50 : (eprop B) => ( (False_ind C) H00) ) ) H61) ) (H5 H11) ) ) (H60 H40) ) ) (H0 H11) ) ) (H6 H40) ) ) ) H2) ) (H20 H40) ) ) ) H1) ) (H10 H40) ) ) ) (H40 : (eprop C) => ( (H1 : (eprop (not A) ) => ( (H00 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H50 : (eprop A) => ( (H01 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) C) (H11 : (eprop A) => ( (H02 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H21 : (eprop A) => ( (H03 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind C) H60) ) (H1 H50) ) ) (H6 H50) ) ) ) (H21 : (eprop B) => ( (H03 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind C) H60) ) (H1 H50) ) ) (H6 H50) ) ) ) H02) ) (H20 H50) ) ) ) (H11 : (eprop C) => ( (H02 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) C) (H21 : (eprop A) => ( (H03 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind C) H60) ) (H1 H50) ) ) (H6 H50) ) ) ) (H21 : (eprop B) => ( (H03 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind C) H60) ) (H1 H50) ) ) (H6 H50) ) ) ) H02) ) (H20 H50) ) ) ) H01) ) (H10 H50) ) ) ) (H50 : (eprop B) => H40) ) H00) ) (H5 H40) ) ) (H0 H40) ) ) ) H0) ) (H4 H30) ) ) (H H30) ) ) ) (H30 : (eprop C) => ( (H6 : (eprop (not A) ) => ( (H00 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) B) (H50 : (eprop A) => ( (H01 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) B) (H11 : (eprop A) => ( (H02 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) B) (H21 : (eprop A) => ( (H03 : (eprop False) => ( (False_ind B) H03) ) (H6 H50) ) ) ) (H21 : (eprop B) => ( (H03 : (eprop False) => ( (H60 : (eprop (not A) ) => ( (H0 : (eprop False) => ( (H61 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) B) (H40 : (eprop A) => ( (False_ind B) H0) ) ) (H40 : (eprop C) => ( (False_ind B) H0) ) ) H61) ) (H4 H21) ) ) (H60 H50) ) ) (H H21) ) ) (H6 H50) ) ) ) H02) ) (H20 H50) ) ) ) (H11 : (eprop C) => ( (H02 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) B) (H21 : (eprop A) => ( (H03 : (eprop False) => ( (False_ind B) H03) ) (H6 H50) ) ) ) (H21 : (eprop B) => ( (H03 : (eprop False) => ( (H60 : (eprop (not A) ) => ( (H0 : (eprop False) => ( (H61 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) B) (H40 : (eprop A) => ( (False_ind B) H0) ) ) (H40 : (eprop C) => ( (False_ind B) H0) ) ) H61) ) (H4 H21) ) ) (H60 H50) ) ) (H H21) ) ) (H6 H50) ) ) ) H02) ) (H20 H50) ) ) ) H01) ) (H10 H50) ) ) ) (H50 : (eprop B) => ( (H01 : (eprop (not A) ) => ( (H0 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) B) (H40 : (eprop A) => ( (H1 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) B) (H11 : (eprop A) => ( (H2 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) B) (H21 : (eprop A) => ( (H3 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind B) H60) ) (H01 H40) ) ) (H6 H40) ) ) ) (H21 : (eprop B) => ( (H3 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind B) H60) ) (H01 H40) ) ) (H6 H40) ) ) ) H2) ) (H20 H40) ) ) ) (H11 : (eprop C) => ( (H2 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) B) (H21 : (eprop A) => ( (H3 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind B) H60) ) (H01 H40) ) ) (H6 H40) ) ) ) (H21 : (eprop B) => ( (H3 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind B) H60) ) (H01 H40) ) ) (H6 H40) ) ) ) H2) ) (H20 H40) ) ) ) H1) ) (H10 H40) ) ) ) (H40 : (eprop C) => H50) ) H0) ) (H4 H50) ) ) (H H50) ) ) ) H00) ) (H5 H30) ) ) (H0 H30) ) ) ) ) (H5 : (eprop C) => (H3 ( ( (or_intror A) C) H5) ) ) ) ) (H20 : (eprop A) => (H3 ( ( (or_introl A) C) H20) ) ) ) ) (H4 : (eprop B) => (H2 ( ( (or_intror A) B) H4) ) ) ) ) (H10 : (eprop A) => (H2 ( ( (or_introl A) B) H10) ) ) ) ) ) ) H1) ) ) (H1 : (eprop ( (iff B) C) ) => ( ( ( ( (and_ind ( (dotpipp B) (_145 : (eprop B) => C) ) ) ( (dotpipp C) (_146 : (eprop C) => B) ) ) ( (iff ( (or A) B) ) ( (or A) C) ) ) (H2 : (eprop ( (dotpipp B) (_150 : (eprop B) => C) ) ) => (H3 : (eprop ( (dotpipp C) (_149 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (or A) B) ) (_147 : (eprop ( (or A) B) ) => ( (or A) C) ) ) ) ( (dotpipp ( (or A) C) ) (_148 : (eprop ( (or A) C) ) => ( (or A) B) ) ) ) (H10 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) ( (or A) C) ) (H4 : (eprop A) => ( ( (or_introl A) C) H4) ) ) (H4 : (eprop B) => ( (H11 : (eprop (not A) ) => ( (H0 : (eprop C) => ( (H20 : (eprop (not A) ) => ( (H00 : (eprop B) => ( ( (or_intror A) C) H0) ) (H3 H0) ) ) (H0 H0) ) ) (H2 H4) ) ) (H H4) ) ) ) H10) ) ) (H10 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) ( (or A) B) ) (H4 : (eprop A) => ( ( (or_introl A) B) H4) ) ) (H4 : (eprop C) => ( (H11 : (eprop (not A) ) => ( (H00 : (eprop B) => ( (H30 : (eprop (not A) ) => ( (H0 : (eprop C) => ( ( (or_intror A) B) H00) ) (H2 H00) ) ) (H H00) ) ) (H3 H4) ) ) (H0 H4) ) ) ) H10) ) ) ) ) ) H1) ) ) ) ) ) ) ) .
or_cancel_r : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_180 : (_177 : (eprop B) -> (eprop (not A) ) ) -> (_179 : (_178 : (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) (_176 : (eprop B) => (not A) ) ) ) => (H0 : (eprop ( (dotpipp C) (_175 : (eprop C) => (not A) ) ) ) => ( ( ( (conj ( (dotpipp ( (iff ( (or B) A) ) ( (or C) A) ) ) (_157 : (eprop ( (iff ( (or B) A) ) ( (or C) A) ) ) => ( (iff B) C) ) ) ) ( (dotpipp ( (iff B) C) ) (_158 : (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) ) (_159 : (eprop ( (or B) A) ) => ( (or C) A) ) ) ) ( (dotpipp ( (or C) A) ) (_160 : (eprop ( (or C) A) ) => ( (or B) A) ) ) ) ( (iff B) C) ) (H2 : (eprop ( (dotpipp ( (or B) A) ) (_168 : (eprop ( (or B) A) ) => ( (or C) A) ) ) ) => (H3 : (eprop ( (dotpipp ( (or C) A) ) (_167 : (eprop ( (or C) A) ) => ( (or B) A) ) ) ) => ( (H10 : (eprop ( (dotpipp B) (_166 : (eprop B) => ( (or C) A) ) ) ) => ( (H4 : (eprop ( (dotpipp A) (_165 : (eprop A) => ( (or C) A) ) ) ) => ( (H20 : (eprop ( (dotpipp C) (_164 : (eprop C) => ( (or B) A) ) ) ) => ( (H5 : (eprop ( (dotpipp A) (_163 : (eprop A) => ( (or B) A) ) ) ) => ( ( ( (conj ( (dotpipp B) (_161 : (eprop B) => C) ) ) ( (dotpipp C) (_162 : (eprop C) => B) ) ) (H30 : (eprop B) => ( (H6 : (eprop (not A) ) => ( (H0 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) C) (H11 : (eprop C) => ( (H1 : (eprop (not A) ) => ( (H00 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H21 : (eprop B) => H11) ) (H21 : (eprop A) => ( (H01 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) C) (H40 : (eprop C) => ( (H02 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H50 : (eprop B) => ( (H03 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind C) H60) ) (H1 H21) ) ) (H6 H21) ) ) ) (H50 : (eprop A) => ( (H03 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind C) H60) ) (H1 H21) ) ) (H6 H21) ) ) ) H02) ) (H5 H21) ) ) ) (H40 : (eprop A) => ( (H02 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H50 : (eprop B) => ( (H03 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind C) H60) ) (H1 H21) ) ) (H6 H21) ) ) ) (H50 : (eprop A) => ( (H03 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind C) H60) ) (H1 H21) ) ) (H6 H21) ) ) ) H02) ) (H5 H21) ) ) ) H01) ) (H4 H21) ) ) ) H00) ) (H20 H11) ) ) (H0 H11) ) ) ) (H11 : (eprop A) => ( (H1 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) C) (H40 : (eprop C) => ( (H2 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H50 : (eprop B) => ( (H3 : (eprop False) => ( (H60 : (eprop (not A) ) => ( (H00 : (eprop False) => ( (H61 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H21 : (eprop B) => ( (False_ind C) H00) ) ) (H21 : (eprop A) => ( (False_ind C) H00) ) ) H61) ) (H20 H40) ) ) (H60 H11) ) ) (H0 H40) ) ) (H6 H11) ) ) ) (H50 : (eprop A) => ( (H3 : (eprop False) => ( (H60 : (eprop (not A) ) => ( (H00 : (eprop False) => ( (H61 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H21 : (eprop B) => ( (False_ind C) H00) ) ) (H21 : (eprop A) => ( (False_ind C) H00) ) ) H61) ) (H20 H40) ) ) (H60 H11) ) ) (H0 H40) ) ) (H6 H11) ) ) ) H2) ) (H5 H11) ) ) ) (H40 : (eprop A) => ( (H2 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) C) (H50 : (eprop B) => ( (H3 : (eprop False) => ( (False_ind C) H3) ) (H6 H11) ) ) ) (H50 : (eprop A) => ( (H3 : (eprop False) => ( (False_ind C) H3) ) (H6 H11) ) ) ) H2) ) (H5 H11) ) ) ) H1) ) (H4 H11) ) ) ) H0) ) (H10 H30) ) ) (H H30) ) ) ) (H30 : (eprop C) => ( (H6 : (eprop (not A) ) => ( (H00 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) B) (H21 : (eprop B) => ( (H01 : (eprop (not A) ) => ( (H0 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) B) (H11 : (eprop C) => H21) ) (H11 : (eprop A) => ( (H1 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) B) (H40 : (eprop C) => ( (H2 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) B) (H50 : (eprop B) => ( (H3 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind B) H60) ) (H01 H11) ) ) (H6 H11) ) ) ) (H50 : (eprop A) => ( (H3 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind B) H60) ) (H01 H11) ) ) (H6 H11) ) ) ) H2) ) (H5 H11) ) ) ) (H40 : (eprop A) => ( (H2 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) B) (H50 : (eprop B) => ( (H3 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind B) H60) ) (H01 H11) ) ) (H6 H11) ) ) ) (H50 : (eprop A) => ( (H3 : (eprop False) => ( (H60 : (eprop False) => ( (False_ind B) H60) ) (H01 H11) ) ) (H6 H11) ) ) ) H2) ) (H5 H11) ) ) ) H1) ) (H4 H11) ) ) ) H0) ) (H10 H21) ) ) (H H21) ) ) ) (H21 : (eprop A) => ( (H01 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) B) (H40 : (eprop C) => ( (H02 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) B) (H50 : (eprop B) => ( (H03 : (eprop False) => ( (H60 : (eprop (not A) ) => ( (H0 : (eprop False) => ( (H61 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) B) (H11 : (eprop C) => ( (False_ind B) H0) ) ) (H11 : (eprop A) => ( (False_ind B) H0) ) ) H61) ) (H10 H50) ) ) (H60 H21) ) ) (H H50) ) ) (H6 H21) ) ) ) (H50 : (eprop A) => ( (H03 : (eprop False) => ( (False_ind B) H03) ) (H6 H21) ) ) ) H02) ) (H5 H21) ) ) ) (H40 : (eprop A) => ( (H02 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) B) (H50 : (eprop B) => ( (H03 : (eprop False) => ( (H60 : (eprop (not A) ) => ( (H0 : (eprop False) => ( (H61 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) B) (H11 : (eprop C) => ( (False_ind B) H0) ) ) (H11 : (eprop A) => ( (False_ind B) H0) ) ) H61) ) (H10 H50) ) ) (H60 H21) ) ) (H H50) ) ) (H6 H21) ) ) ) (H50 : (eprop A) => ( (H03 : (eprop False) => ( (False_ind B) H03) ) (H6 H21) ) ) ) H02) ) (H5 H21) ) ) ) H01) ) (H4 H21) ) ) ) H00) ) (H20 H30) ) ) (H0 H30) ) ) ) ) (H5 : (eprop A) => (H3 ( ( (or_intror C) A) H5) ) ) ) ) (H20 : (eprop C) => (H3 ( ( (or_introl C) A) H20) ) ) ) ) (H4 : (eprop A) => (H2 ( ( (or_intror B) A) H4) ) ) ) ) (H10 : (eprop B) => (H2 ( ( (or_introl B) A) H10) ) ) ) ) ) ) H1) ) ) (H1 : (eprop ( (iff B) C) ) => ( ( ( ( (and_ind ( (dotpipp B) (_169 : (eprop B) => C) ) ) ( (dotpipp C) (_170 : (eprop C) => B) ) ) ( (iff ( (or B) A) ) ( (or C) A) ) ) (H2 : (eprop ( (dotpipp B) (_174 : (eprop B) => C) ) ) => (H3 : (eprop ( (dotpipp C) (_173 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (or B) A) ) (_171 : (eprop ( (or B) A) ) => ( (or C) A) ) ) ) ( (dotpipp ( (or C) A) ) (_172 : (eprop ( (or C) A) ) => ( (or B) A) ) ) ) (H10 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) ( (or C) A) ) (H4 : (eprop B) => ( (H11 : (eprop (not A) ) => ( (H0 : (eprop C) => ( (H20 : (eprop (not A) ) => ( (H00 : (eprop B) => ( ( (or_introl C) A) H0) ) (H3 H0) ) ) (H0 H0) ) ) (H2 H4) ) ) (H H4) ) ) ) (H4 : (eprop A) => ( ( (or_intror C) A) H4) ) ) H10) ) ) (H10 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) ( (or B) A) ) (H4 : (eprop C) => ( (H11 : (eprop (not A) ) => ( (H00 : (eprop B) => ( (H30 : (eprop (not A) ) => ( (H0 : (eprop C) => ( ( (or_introl B) A) H00) ) (H2 H00) ) ) (H H00) ) ) (H3 H4) ) ) (H0 H4) ) ) ) (H4 : (eprop A) => ( ( (or_intror B) A) H4) ) ) H10) ) ) ) ) ) H1) ) ) ) ) ) ) ) .
and_iff_compat_l : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_187 : (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) (_181 : (eprop B) => C) ) ) ( (dotpipp C) (_182 : (eprop C) => B) ) ) ( (iff ( (and A) B) ) ( (and A) C) ) ) (H0 : (eprop ( (dotpipp B) (_186 : (eprop B) => C) ) ) => (H1 : (eprop ( (dotpipp C) (_185 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (and A) B) ) (_183 : (eprop ( (and A) B) ) => ( (and A) C) ) ) ) ( (dotpipp ( (and A) C) ) (_184 : (eprop ( (and A) C) ) => ( (and A) B) ) ) ) (H0 : (eprop ( (and A) B) ) => ( ( ( ( (and_ind A) B) ( (and A) C) ) (H2 : (eprop A) => (H3 : (eprop B) => ( (H1 : (eprop C) => ( (H00 : (eprop B) => ( ( ( (conj A) C) H2) H1) ) (H1 H1) ) ) (H0 H3) ) ) ) ) H0) ) ) (H0 : (eprop ( (and A) C) ) => ( ( ( ( (and_ind A) C) ( (and A) B) ) (H2 : (eprop A) => (H3 : (eprop C) => ( (H1 : (eprop B) => ( (H10 : (eprop C) => ( ( ( (conj A) B) H2) H1) ) (H0 H1) ) ) (H1 H3) ) ) ) ) H0) ) ) ) ) ) H) ) ) ) ) .
and_iff_compat_r : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_194 : (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) (_188 : (eprop B) => C) ) ) ( (dotpipp C) (_189 : (eprop C) => B) ) ) ( (iff ( (and B) A) ) ( (and C) A) ) ) (H0 : (eprop ( (dotpipp B) (_193 : (eprop B) => C) ) ) => (H1 : (eprop ( (dotpipp C) (_192 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (and B) A) ) (_190 : (eprop ( (and B) A) ) => ( (and C) A) ) ) ) ( (dotpipp ( (and C) A) ) (_191 : (eprop ( (and C) A) ) => ( (and B) A) ) ) ) (H0 : (eprop ( (and B) A) ) => ( ( ( ( (and_ind B) A) ( (and C) A) ) (H2 : (eprop B) => (H3 : (eprop A) => ( (H1 : (eprop C) => ( (H00 : (eprop B) => ( ( ( (conj C) A) H1) H3) ) (H1 H1) ) ) (H0 H2) ) ) ) ) H0) ) ) (H0 : (eprop ( (and C) A) ) => ( ( ( ( (and_ind C) A) ( (and B) A) ) (H2 : (eprop C) => (H3 : (eprop A) => ( (H1 : (eprop B) => ( (H10 : (eprop C) => ( ( ( (conj B) A) H1) H3) ) (H0 H1) ) ) (H1 H2) ) ) ) ) H0) ) ) ) ) ) H) ) ) ) ) .
or_iff_compat_l : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_201 : (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) (_195 : (eprop B) => C) ) ) ( (dotpipp C) (_196 : (eprop C) => B) ) ) ( (iff ( (or A) B) ) ( (or A) C) ) ) (H0 : (eprop ( (dotpipp B) (_200 : (eprop B) => C) ) ) => (H1 : (eprop ( (dotpipp C) (_199 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (or A) B) ) (_197 : (eprop ( (or A) B) ) => ( (or A) C) ) ) ) ( (dotpipp ( (or A) C) ) (_198 : (eprop ( (or A) C) ) => ( (or A) B) ) ) ) (H0 : (eprop ( (or A) B) ) => ( ( ( ( ( (or_ind A) B) ( (or A) C) ) (H2 : (eprop A) => ( ( (or_introl A) C) H2) ) ) (H2 : (eprop B) => ( (H1 : (eprop C) => ( (H00 : (eprop B) => ( ( (or_intror A) C) H1) ) (H1 H1) ) ) (H0 H2) ) ) ) H0) ) ) (H0 : (eprop ( (or A) C) ) => ( ( ( ( ( (or_ind A) C) ( (or A) B) ) (H2 : (eprop A) => ( ( (or_introl A) B) H2) ) ) (H2 : (eprop C) => ( (H1 : (eprop B) => ( (H10 : (eprop C) => ( ( (or_intror A) B) H1) ) (H0 H1) ) ) (H1 H2) ) ) ) H0) ) ) ) ) ) H) ) ) ) ) .
or_iff_compat_r : (A : Uprop -> (B : Uprop -> (C : Uprop -> (_208 : (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) (_202 : (eprop B) => C) ) ) ( (dotpipp C) (_203 : (eprop C) => B) ) ) ( (iff ( (or B) A) ) ( (or C) A) ) ) (H0 : (eprop ( (dotpipp B) (_207 : (eprop B) => C) ) ) => (H1 : (eprop ( (dotpipp C) (_206 : (eprop C) => B) ) ) => ( ( ( (conj ( (dotpipp ( (or B) A) ) (_204 : (eprop ( (or B) A) ) => ( (or C) A) ) ) ) ( (dotpipp ( (or C) A) ) (_205 : (eprop ( (or C) A) ) => ( (or B) A) ) ) ) (H0 : (eprop ( (or B) A) ) => ( ( ( ( ( (or_ind B) A) ( (or C) A) ) (H2 : (eprop B) => ( (H1 : (eprop C) => ( (H00 : (eprop B) => ( ( (or_introl C) A) H1) ) (H1 H1) ) ) (H0 H2) ) ) ) (H2 : (eprop A) => ( ( (or_intror C) A) H2) ) ) H0) ) ) (H0 : (eprop ( (or C) A) ) => ( ( ( ( ( (or_ind C) A) ( (or B) A) ) (H2 : (eprop C) => ( (H1 : (eprop B) => ( (H10 : (eprop C) => ( ( (or_introl B) A) H1) ) (H0 H1) ) ) (H1 H2) ) ) ) (H2 : (eprop A) => ( ( (or_intror B) A) H2) ) ) H0) ) ) ) ) ) H) ) ) ) ) .
case_10 : (A : Uprop -> (B : Uprop -> (H : (eprop ( (iff A) B) ) -> (_213 : (eprop ( (and ( (dotpipp A) (_209 : (eprop A) => B) ) ) ( (dotpipp B) (_210 : (eprop B) => A) ) ) ) -> (eprop ( (and ( (dotpipp A) (_211 : (eprop A) => B) ) ) ( (dotpipp B) (_212 : (eprop B) => A) ) ) ) ) ) ) ) .
[A : Uprop, B : Uprop, H : (eprop ( (iff A) B) ) , var_16 : (eprop A) , var_17 : (eprop B) ] ( ( ( (case_10 A) B) H) ( ( ( (conj A) B) var_16) var_17) ) --> ( ( (H0 : (eprop ( (dotpipp A) (_217 : (eprop A) => B) ) ) => (H0 : (eprop ( (dotpipp B) (_216 : (eprop B) => A) ) ) => ( ( ( (conj ( (dotpipp A) (_214 : (eprop A) => B) ) ) ( (dotpipp B) (_215 : (eprop B) => A) ) ) H0) H0) ) ) var_16) var_17) .
iff_and : (A : Uprop -> (B : Uprop -> (_220 : (eprop ( (iff A) B) ) -> (eprop ( (and ( (dotpipp A) (_218 : (eprop A) => B) ) ) ( (dotpipp B) (_219 : (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) (_243 : (eprop A) => B) ) ) ( (dotpipp B) (_244 : (eprop B) => A) ) ) ) ) ) ) .
[] iff_to_and --> (A : (etype dotprop) => (B : (etype dotprop) => ( ( ( (conj ( (dotpipp ( (iff A) B) ) (_223 : (eprop ( (iff A) B) ) => ( (and ( (dotpipp A) (_221 : (eprop A) => B) ) ) ( (dotpipp B) (_222 : (eprop B) => A) ) ) ) ) ) ( (dotpipp ( (and ( (dotpipp A) (_224 : (eprop A) => B) ) ) ( (dotpipp B) (_225 : (eprop B) => A) ) ) ) (_226 : (eprop ( (and ( (dotpipp A) (_224 : (eprop A) => B) ) ) ( (dotpipp B) (_225 : (eprop B) => A) ) ) ) => ( (iff A) B) ) ) ) (H : (eprop ( (iff A) B) ) => ( ( ( ( (and_ind ( (dotpipp A) (_227 : (eprop A) => B) ) ) ( (dotpipp B) (_228 : (eprop B) => A) ) ) ( (and ( (dotpipp A) (_229 : (eprop A) => B) ) ) ( (dotpipp B) (_230 : (eprop B) => A) ) ) ) (H0 : (eprop ( (dotpipp A) (_234 : (eprop A) => B) ) ) => (H1 : (eprop ( (dotpipp B) (_233 : (eprop B) => A) ) ) => ( ( ( (conj ( (dotpipp A) (_231 : (eprop A) => B) ) ) ( (dotpipp B) (_232 : (eprop B) => A) ) ) (H0 : (eprop A) => ( (H2 : (eprop B) => ( (H00 : (eprop A) => H2) (H1 H2) ) ) (H0 H0) ) ) ) (H0 : (eprop B) => ( (H2 : (eprop A) => ( (H10 : (eprop B) => H2) (H0 H2) ) ) (H1 H0) ) ) ) ) ) ) H) ) ) (H : (eprop ( (and ( (dotpipp A) (_241 : (eprop A) => B) ) ) ( (dotpipp B) (_242 : (eprop B) => A) ) ) ) => ( ( ( ( (and_ind ( (dotpipp A) (_235 : (eprop A) => B) ) ) ( (dotpipp B) (_236 : (eprop B) => A) ) ) ( (iff A) B) ) (H0 : (eprop ( (dotpipp A) (_240 : (eprop A) => B) ) ) => (H1 : (eprop ( (dotpipp B) (_239 : (eprop B) => A) ) ) => ( ( ( (conj ( (dotpipp A) (_237 : (eprop A) => B) ) ) ( (dotpipp B) (_238 : (eprop B) => A) ) ) (H0 : (eprop A) => ( (H2 : (eprop B) => ( (H00 : (eprop A) => H2) (H1 H2) ) ) (H0 H0) ) ) ) (H0 : (eprop B) => ( (H2 : (eprop A) => ( (H10 : (eprop B) => H2) (H0 H2) ) ) (H1 H0) ) ) ) ) ) ) H) ) ) ) ) .