DEFINITION terms_props__kind_dec()
TYPE =
∀k1:K.∀k2:K.(or (eq K k1 k2) (eq K k1 k2)→∀P:Prop.P)
BODY =
assume k1: K
we proceed by induction on k1 to prove ∀k2:K.(or (eq K k1 k2) (eq K k1 k2)→∀P:Prop.P)
case Bind : b:B ⇒
the thesis becomes ∀k2:K.(or (eq K (Bind b) k2) (eq K (Bind b) k2)→∀P:Prop.P)
assume k2: K
we proceed by induction on k2 to prove or (eq K (Bind b) k2) (eq K (Bind b) k2)→∀P:Prop.P
case Bind : b0:B ⇒
the thesis becomes
or
eq K (Bind b) (Bind b0)
(eq K (Bind b) (Bind b0))→∀P:Prop.P
(H_x)
by (terms_props__bind_dec . .)
or (eq B b b0) (eq B b b0)→∀P:Prop.P
end of H_x
(H) consider H_x
we proceed by induction on H to prove
or
eq K (Bind b) (Bind b0)
(eq K (Bind b) (Bind b0))→∀P:Prop.P
case or_introl : H0:eq B b b0 ⇒
the thesis becomes
or
eq K (Bind b) (Bind b0)
(eq K (Bind b) (Bind b0))→∀P:Prop.P
we proceed by induction on H0 to prove
or
eq K (Bind b) (Bind b0)
(eq K (Bind b) (Bind b0))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes
or
eq K (Bind b) (Bind b)
(eq K (Bind b) (Bind b))→∀P:Prop.P
by (refl_equal . .)
we proved eq K (Bind b) (Bind b)
by (or_introl . . previous)
or
eq K (Bind b) (Bind b)
(eq K (Bind b) (Bind b))→∀P:Prop.P
or
eq K (Bind b) (Bind b0)
(eq K (Bind b) (Bind b0))→∀P:Prop.P
case or_intror : H0:(eq B b b0)→∀P:Prop.P ⇒
the thesis becomes
or
eq K (Bind b) (Bind b0)
(eq K (Bind b) (Bind b0))→∀P:Prop.P
suppose H1: eq K (Bind b) (Bind b0)
assume P: Prop
(H2)
by (f_equal . . . . . H1)
we proved
eq
B
<λ:K.B> CASE Bind b OF Bind b1⇒b1 | Flat ⇒b
<λ:K.B> CASE Bind b0 OF Bind b1⇒b1 | Flat ⇒b
eq
B
λe:K.<λ:K.B> CASE e OF Bind b1⇒b1 | Flat ⇒b (Bind b)
λe:K.<λ:K.B> CASE e OF Bind b1⇒b1 | Flat ⇒b (Bind b0)
end of H2
(H3)
consider H2
we proved
eq
B
<λ:K.B> CASE Bind b OF Bind b1⇒b1 | Flat ⇒b
<λ:K.B> CASE Bind b0 OF Bind b1⇒b1 | Flat ⇒b
that is equivalent to eq B b b0
by (eq_ind_r . . . H0 . previous)
(eq B b b)→∀P0:Prop.P0
end of H3
by (refl_equal . .)
we proved eq B b b
by (H3 previous .)
we proved P
we proved (eq K (Bind b) (Bind b0))→∀P:Prop.P
by (or_intror . . previous)
or
eq K (Bind b) (Bind b0)
(eq K (Bind b) (Bind b0))→∀P:Prop.P
or
eq K (Bind b) (Bind b0)
(eq K (Bind b) (Bind b0))→∀P:Prop.P
case Flat : f:F ⇒
the thesis becomes
or
eq K (Bind b) (Flat f)
(eq K (Bind b) (Flat f))→∀P:Prop.P
suppose H: eq K (Bind b) (Flat f)
assume P: Prop
(H0)
we proceed by induction on H to prove <λ:K.Prop> CASE Flat f OF Bind ⇒True | Flat ⇒False
case refl_equal : ⇒
the thesis becomes <λ:K.Prop> CASE Bind b OF Bind ⇒True | Flat ⇒False
consider I
we proved True
<λ:K.Prop> CASE Bind b OF Bind ⇒True | Flat ⇒False
<λ:K.Prop> CASE Flat f OF Bind ⇒True | Flat ⇒False
end of H0
consider H0
we proved <λ:K.Prop> CASE Flat f OF Bind ⇒True | Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq K (Bind b) (Flat f))→∀P:Prop.P
by (or_intror . . previous)
or
eq K (Bind b) (Flat f)
(eq K (Bind b) (Flat f))→∀P:Prop.P
we proved or (eq K (Bind b) k2) (eq K (Bind b) k2)→∀P:Prop.P
∀k2:K.(or (eq K (Bind b) k2) (eq K (Bind b) k2)→∀P:Prop.P)
case Flat : f:F ⇒
the thesis becomes ∀k2:K.(or (eq K (Flat f) k2) (eq K (Flat f) k2)→∀P:Prop.P)
assume k2: K
we proceed by induction on k2 to prove or (eq K (Flat f) k2) (eq K (Flat f) k2)→∀P:Prop.P
case Bind : b:B ⇒
the thesis becomes
or
eq K (Flat f) (Bind b)
(eq K (Flat f) (Bind b))→∀P:Prop.P
suppose H: eq K (Flat f) (Bind b)
assume P: Prop
(H0)
we proceed by induction on H to prove <λ:K.Prop> CASE Bind b OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes <λ:K.Prop> CASE Flat f OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:K.Prop> CASE Flat f OF Bind ⇒False | Flat ⇒True
<λ:K.Prop> CASE Bind b OF Bind ⇒False | Flat ⇒True
end of H0
consider H0
we proved <λ:K.Prop> CASE Bind b OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq K (Flat f) (Bind b))→∀P:Prop.P
by (or_intror . . previous)
or
eq K (Flat f) (Bind b)
(eq K (Flat f) (Bind b))→∀P:Prop.P
case Flat : f0:F ⇒
the thesis becomes
or
eq K (Flat f) (Flat f0)
(eq K (Flat f) (Flat f0))→∀P:Prop.P
(H_x)
by (terms_props__flat_dec . .)
or (eq F f f0) (eq F f f0)→∀P:Prop.P
end of H_x
(H) consider H_x
we proceed by induction on H to prove
or
eq K (Flat f) (Flat f0)
(eq K (Flat f) (Flat f0))→∀P:Prop.P
case or_introl : H0:eq F f f0 ⇒
the thesis becomes
or
eq K (Flat f) (Flat f0)
(eq K (Flat f) (Flat f0))→∀P:Prop.P
we proceed by induction on H0 to prove
or
eq K (Flat f) (Flat f0)
(eq K (Flat f) (Flat f0))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes
or
eq K (Flat f) (Flat f)
(eq K (Flat f) (Flat f))→∀P:Prop.P
by (refl_equal . .)
we proved eq K (Flat f) (Flat f)
by (or_introl . . previous)
or
eq K (Flat f) (Flat f)
(eq K (Flat f) (Flat f))→∀P:Prop.P
or
eq K (Flat f) (Flat f0)
(eq K (Flat f) (Flat f0))→∀P:Prop.P
case or_intror : H0:(eq F f f0)→∀P:Prop.P ⇒
the thesis becomes
or
eq K (Flat f) (Flat f0)
(eq K (Flat f) (Flat f0))→∀P:Prop.P
suppose H1: eq K (Flat f) (Flat f0)
assume P: Prop
(H2)
by (f_equal . . . . . H1)
we proved
eq
F
<λ:K.F> CASE Flat f OF Bind ⇒f | Flat f1⇒f1
<λ:K.F> CASE Flat f0 OF Bind ⇒f | Flat f1⇒f1
eq
F
λe:K.<λ:K.F> CASE e OF Bind ⇒f | Flat f1⇒f1 (Flat f)
λe:K.<λ:K.F> CASE e OF Bind ⇒f | Flat f1⇒f1 (Flat f0)
end of H2
(H3)
consider H2
we proved
eq
F
<λ:K.F> CASE Flat f OF Bind ⇒f | Flat f1⇒f1
<λ:K.F> CASE Flat f0 OF Bind ⇒f | Flat f1⇒f1
that is equivalent to eq F f f0
by (eq_ind_r . . . H0 . previous)
(eq F f f)→∀P0:Prop.P0
end of H3
by (refl_equal . .)
we proved eq F f f
by (H3 previous .)
we proved P
we proved (eq K (Flat f) (Flat f0))→∀P:Prop.P
by (or_intror . . previous)
or
eq K (Flat f) (Flat f0)
(eq K (Flat f) (Flat f0))→∀P:Prop.P
or
eq K (Flat f) (Flat f0)
(eq K (Flat f) (Flat f0))→∀P:Prop.P
we proved or (eq K (Flat f) k2) (eq K (Flat f) k2)→∀P:Prop.P
∀k2:K.(or (eq K (Flat f) k2) (eq K (Flat f) k2)→∀P:Prop.P)
we proved ∀k2:K.(or (eq K k1 k2) (eq K k1 k2)→∀P:Prop.P)
we proved ∀k1:K.∀k2:K.(or (eq K k1 k2) (eq K k1 k2)→∀P:Prop.P)