DEFINITION ex2_2_ind()
TYPE =
∀A0:Set
.∀A1:Set
.∀P0:A0→A1→Prop
.∀P1:A0→A1→Prop.∀P:Prop.(∀a:A0.∀a1:A1.(P0 a a1)→(P1 a a1)→P)→(ex2_2 A0 A1 P0 P1)→P
BODY =
assume A0: Set
assume A1: Set
assume P0: A0→A1→Prop
assume P1: A0→A1→Prop
assume P: Prop
suppose H: ∀a:A0.∀a1:A1.(P0 a a1)→(P1 a a1)→P
suppose H1: ex2_2 A0 A1 P0 P1
by cases on H1 we prove P
case ex2_2_intro a:A0 a1:A1 H2:P0 a a1 H3:P1 a a1 ⇒
the thesis becomes P
by (H . . H2 H3)
P
we proved P
we proved
∀A0:Set
.∀A1:Set
.∀P0:A0→A1→Prop
.∀P1:A0→A1→Prop.∀P:Prop.(∀a:A0.∀a1:A1.(P0 a a1)→(P1 a a1)→P)→(ex2_2 A0 A1 P0 P1)→P