DEFINITION term_dec()
TYPE =
∀t1:T.∀t2:T.(or (eq T t1 t2) (eq T t1 t2)→∀P:Prop.P)
BODY =
assume t1: T
we proceed by induction on t1 to prove ∀t2:T.(or (eq T t1 t2) (eq T t1 t2)→∀P:Prop.P)
case TSort : n:nat ⇒
the thesis becomes ∀t2:T.(or (eq T (TSort n) t2) (eq T (TSort n) t2)→∀P:Prop.P)
assume t2: T
we proceed by induction on t2 to prove or (eq T (TSort n) t2) (eq T (TSort n) t2)→∀P:Prop.P
case TSort : n0:nat ⇒
the thesis becomes
or
eq T (TSort n) (TSort n0)
(eq T (TSort n) (TSort n0))→∀P:Prop.P
(H_x)
by (nat_dec . .)
or (eq nat n n0) (eq nat n n0)→∀P:Prop.P
end of H_x
(H) consider H_x
we proceed by induction on H to prove
or
eq T (TSort n) (TSort n0)
(eq T (TSort n) (TSort n0))→∀P:Prop.P
case or_introl : H0:eq nat n n0 ⇒
the thesis becomes
or
eq T (TSort n) (TSort n0)
(eq T (TSort n) (TSort n0))→∀P:Prop.P
we proceed by induction on H0 to prove
or
eq T (TSort n) (TSort n0)
(eq T (TSort n) (TSort n0))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes
or
eq T (TSort n) (TSort n)
(eq T (TSort n) (TSort n))→∀P:Prop.P
by (refl_equal . .)
we proved eq T (TSort n) (TSort n)
by (or_introl . . previous)
or
eq T (TSort n) (TSort n)
(eq T (TSort n) (TSort n))→∀P:Prop.P
or
eq T (TSort n) (TSort n0)
(eq T (TSort n) (TSort n0))→∀P:Prop.P
case or_intror : H0:(eq nat n n0)→∀P:Prop.P ⇒
the thesis becomes
or
eq T (TSort n) (TSort n0)
(eq T (TSort n) (TSort n0))→∀P:Prop.P
suppose H1: eq T (TSort n) (TSort n0)
assume P: Prop
(H2)
by (f_equal . . . . . H1)
we proved
eq
nat
<λ:T.nat> CASE TSort n OF TSort n1⇒n1 | TLRef ⇒n | THead ⇒n
<λ:T.nat> CASE TSort n0 OF TSort n1⇒n1 | TLRef ⇒n | THead ⇒n
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort n1⇒n1 | TLRef ⇒n | THead ⇒n (TSort n)
λe:T.<λ:T.nat> CASE e OF TSort n1⇒n1 | TLRef ⇒n | THead ⇒n (TSort n0)
end of H2
(H3)
consider H2
we proved
eq
nat
<λ:T.nat> CASE TSort n OF TSort n1⇒n1 | TLRef ⇒n | THead ⇒n
<λ:T.nat> CASE TSort n0 OF TSort n1⇒n1 | TLRef ⇒n | THead ⇒n
that is equivalent to eq nat n n0
by (eq_ind_r . . . H0 . previous)
(eq nat n n)→∀P0:Prop.P0
end of H3
by (refl_equal . .)
we proved eq nat n n
by (H3 previous .)
we proved P
we proved (eq T (TSort n) (TSort n0))→∀P:Prop.P
by (or_intror . . previous)
or
eq T (TSort n) (TSort n0)
(eq T (TSort n) (TSort n0))→∀P:Prop.P
or
eq T (TSort n) (TSort n0)
(eq T (TSort n) (TSort n0))→∀P:Prop.P
case TLRef : n0:nat ⇒
the thesis becomes
or
eq T (TSort n) (TLRef n0)
(eq T (TSort n) (TLRef n0))→∀P:Prop.P
suppose H: eq T (TSort n) (TLRef n0)
assume P: Prop
(H0)
we proceed by induction on H to prove
<λ:T.Prop>
CASE TLRef n0 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE TLRef n0 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H0
consider H0
we proved
<λ:T.Prop>
CASE TLRef n0 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq T (TSort n) (TLRef n0))→∀P:Prop.P
by (or_intror . . previous)
or
eq T (TSort n) (TLRef n0)
(eq T (TSort n) (TLRef n0))→∀P:Prop.P
case THead : k:K t:T t0:T ⇒
the thesis becomes
or
eq T (TSort n) (THead k t t0)
(eq T (TSort n) (THead k t t0))→∀P:Prop.P
() by induction hypothesis we know or (eq T (TSort n) t) (eq T (TSort n) t)→∀P:Prop.P
() by induction hypothesis we know or (eq T (TSort n) t0) (eq T (TSort n) t0)→∀P:Prop.P
suppose H1: eq T (TSort n) (THead k t t0)
assume P: Prop
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE THead k t t0 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE THead k t t0 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H2
consider H2
we proved
<λ:T.Prop>
CASE THead k t t0 OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq T (TSort n) (THead k t t0))→∀P:Prop.P
by (or_intror . . previous)
or
eq T (TSort n) (THead k t t0)
(eq T (TSort n) (THead k t t0))→∀P:Prop.P
we proved or (eq T (TSort n) t2) (eq T (TSort n) t2)→∀P:Prop.P
∀t2:T.(or (eq T (TSort n) t2) (eq T (TSort n) t2)→∀P:Prop.P)
case TLRef : n:nat ⇒
the thesis becomes ∀t2:T.(or (eq T (TLRef n) t2) (eq T (TLRef n) t2)→∀P:Prop.P)
assume t2: T
we proceed by induction on t2 to prove or (eq T (TLRef n) t2) (eq T (TLRef n) t2)→∀P:Prop.P
case TSort : n0:nat ⇒
the thesis becomes
or
eq T (TLRef n) (TSort n0)
(eq T (TLRef n) (TSort n0))→∀P:Prop.P
suppose H: eq T (TLRef n) (TSort n0)
assume P: Prop
(H0)
we proceed by induction on H to prove
<λ:T.Prop>
CASE TSort n0 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE TSort n0 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H0
consider H0
we proved
<λ:T.Prop>
CASE TSort n0 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq T (TLRef n) (TSort n0))→∀P:Prop.P
by (or_intror . . previous)
or
eq T (TLRef n) (TSort n0)
(eq T (TLRef n) (TSort n0))→∀P:Prop.P
case TLRef : n0:nat ⇒
the thesis becomes
or
eq T (TLRef n) (TLRef n0)
(eq T (TLRef n) (TLRef n0))→∀P:Prop.P
(H_x)
by (nat_dec . .)
or (eq nat n n0) (eq nat n n0)→∀P:Prop.P
end of H_x
(H) consider H_x
we proceed by induction on H to prove
or
eq T (TLRef n) (TLRef n0)
(eq T (TLRef n) (TLRef n0))→∀P:Prop.P
case or_introl : H0:eq nat n n0 ⇒
the thesis becomes
or
eq T (TLRef n) (TLRef n0)
(eq T (TLRef n) (TLRef n0))→∀P:Prop.P
we proceed by induction on H0 to prove
or
eq T (TLRef n) (TLRef n0)
(eq T (TLRef n) (TLRef n0))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes
or
eq T (TLRef n) (TLRef n)
(eq T (TLRef n) (TLRef n))→∀P:Prop.P
by (refl_equal . .)
we proved eq T (TLRef n) (TLRef n)
by (or_introl . . previous)
or
eq T (TLRef n) (TLRef n)
(eq T (TLRef n) (TLRef n))→∀P:Prop.P
or
eq T (TLRef n) (TLRef n0)
(eq T (TLRef n) (TLRef n0))→∀P:Prop.P
case or_intror : H0:(eq nat n n0)→∀P:Prop.P ⇒
the thesis becomes
or
eq T (TLRef n) (TLRef n0)
(eq T (TLRef n) (TLRef n0))→∀P:Prop.P
suppose H1: eq T (TLRef n) (TLRef n0)
assume P: Prop
(H2)
by (f_equal . . . . . H1)
we proved
eq
nat
<λ:T.nat> CASE TLRef n OF TSort ⇒n | TLRef n1⇒n1 | THead ⇒n
<λ:T.nat> CASE TLRef n0 OF TSort ⇒n | TLRef n1⇒n1 | THead ⇒n
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort ⇒n | TLRef n1⇒n1 | THead ⇒n (TLRef n)
λe:T.<λ:T.nat> CASE e OF TSort ⇒n | TLRef n1⇒n1 | THead ⇒n (TLRef n0)
end of H2
(H3)
consider H2
we proved
eq
nat
<λ:T.nat> CASE TLRef n OF TSort ⇒n | TLRef n1⇒n1 | THead ⇒n
<λ:T.nat> CASE TLRef n0 OF TSort ⇒n | TLRef n1⇒n1 | THead ⇒n
that is equivalent to eq nat n n0
by (eq_ind_r . . . H0 . previous)
(eq nat n n)→∀P0:Prop.P0
end of H3
by (refl_equal . .)
we proved eq nat n n
by (H3 previous .)
we proved P
we proved (eq T (TLRef n) (TLRef n0))→∀P:Prop.P
by (or_intror . . previous)
or
eq T (TLRef n) (TLRef n0)
(eq T (TLRef n) (TLRef n0))→∀P:Prop.P
or
eq T (TLRef n) (TLRef n0)
(eq T (TLRef n) (TLRef n0))→∀P:Prop.P
case THead : k:K t:T t0:T ⇒
the thesis becomes
or
eq T (TLRef n) (THead k t t0)
(eq T (TLRef n) (THead k t t0))→∀P:Prop.P
() by induction hypothesis we know or (eq T (TLRef n) t) (eq T (TLRef n) t)→∀P:Prop.P
() by induction hypothesis we know or (eq T (TLRef n) t0) (eq T (TLRef n) t0)→∀P:Prop.P
suppose H1: eq T (TLRef n) (THead k t t0)
assume P: Prop
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE THead k t t0 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead k t t0 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H2
consider H2
we proved
<λ:T.Prop>
CASE THead k t t0 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq T (TLRef n) (THead k t t0))→∀P:Prop.P
by (or_intror . . previous)
or
eq T (TLRef n) (THead k t t0)
(eq T (TLRef n) (THead k t t0))→∀P:Prop.P
we proved or (eq T (TLRef n) t2) (eq T (TLRef n) t2)→∀P:Prop.P
∀t2:T.(or (eq T (TLRef n) t2) (eq T (TLRef n) t2)→∀P:Prop.P)
case THead : k:K t:T t0:T ⇒
the thesis becomes ∀t2:T.(or (eq T (THead k t t0) t2) (eq T (THead k t t0) t2)→∀P:Prop.P)
(H) by induction hypothesis we know ∀t2:T.(or (eq T t t2) (eq T t t2)→∀P:Prop.P)
(H0) by induction hypothesis we know ∀t2:T.(or (eq T t0 t2) (eq T t0 t2)→∀P:Prop.P)
assume t2: T
we proceed by induction on t2 to prove or (eq T (THead k t t0) t2) (eq T (THead k t t0) t2)→∀P:Prop.P
case TSort : n:nat ⇒
the thesis becomes
or
eq T (THead k t t0) (TSort n)
(eq T (THead k t t0) (TSort n))→∀P:Prop.P
suppose H1: eq T (THead k t t0) (TSort n)
assume P: Prop
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead k t t0 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead k t t0 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H2
consider H2
we proved
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq T (THead k t t0) (TSort n))→∀P:Prop.P
by (or_intror . . previous)
or
eq T (THead k t t0) (TSort n)
(eq T (THead k t t0) (TSort n))→∀P:Prop.P
case TLRef : n:nat ⇒
the thesis becomes
or
eq T (THead k t t0) (TLRef n)
(eq T (THead k t t0) (TLRef n))→∀P:Prop.P
suppose H1: eq T (THead k t t0) (TLRef n)
assume P: Prop
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead k t t0 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead k t t0 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H2
consider H2
we proved
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq T (THead k t t0) (TLRef n))→∀P:Prop.P
by (or_intror . . previous)
or
eq T (THead k t t0) (TLRef n)
(eq T (THead k t t0) (TLRef n))→∀P:Prop.P
case THead : k0:K t3:T t4:T ⇒
the thesis becomes
or
eq T (THead k t t0) (THead k0 t3 t4)
(eq T (THead k t t0) (THead k0 t3 t4))→∀P:Prop.P
(H1) by induction hypothesis we know or (eq T (THead k t t0) t3) (eq T (THead k t t0) t3)→∀P:Prop.P
(H2) by induction hypothesis we know or (eq T (THead k t t0) t4) (eq T (THead k t t0) t4)→∀P:Prop.P
(H_x)
by (H .)
or (eq T t t3) (eq T t t3)→∀P:Prop.P
end of H_x
(H3) consider H_x
we proceed by induction on H3 to prove
or
eq T (THead k t t0) (THead k0 t3 t4)
(eq T (THead k t t0) (THead k0 t3 t4))→∀P:Prop.P
case or_introl : H4:eq T t t3 ⇒
the thesis becomes
or
eq T (THead k t t0) (THead k0 t3 t4)
(eq T (THead k t t0) (THead k0 t3 t4))→∀P:Prop.P
we proceed by induction on H4 to prove
or
eq T (THead k t t0) (THead k0 t3 t4)
(eq T (THead k t t0) (THead k0 t3 t4))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes
or
eq T (THead k t t0) (THead k0 t t4)
(eq T (THead k t t0) (THead k0 t t4))→∀P:Prop.P
(H_x0)
by (H0 .)
or (eq T t0 t4) (eq T t0 t4)→∀P:Prop.P
end of H_x0
(H6) consider H_x0
we proceed by induction on H6 to prove
or
eq T (THead k t t0) (THead k0 t t4)
(eq T (THead k t t0) (THead k0 t t4))→∀P:Prop.P
case or_introl : H7:eq T t0 t4 ⇒
the thesis becomes
or
eq T (THead k t t0) (THead k0 t t4)
(eq T (THead k t t0) (THead k0 t t4))→∀P:Prop.P
we proceed by induction on H7 to prove
or
eq T (THead k t t0) (THead k0 t t4)
(eq T (THead k t t0) (THead k0 t t4))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes
or
eq T (THead k t t0) (THead k0 t t0)
(eq T (THead k t t0) (THead k0 t t0))→∀P:Prop.P
(H_x1)
by (terms_props__kind_dec . .)
or (eq K k k0) (eq K k k0)→∀P:Prop.P
end of H_x1
(H9) consider H_x1
we proceed by induction on H9 to prove
or
eq T (THead k t t0) (THead k0 t t0)
(eq T (THead k t t0) (THead k0 t t0))→∀P:Prop.P
case or_introl : H10:eq K k k0 ⇒
the thesis becomes
or
eq T (THead k t t0) (THead k0 t t0)
(eq T (THead k t t0) (THead k0 t t0))→∀P:Prop.P
we proceed by induction on H10 to prove
or
eq T (THead k t t0) (THead k0 t t0)
(eq T (THead k t t0) (THead k0 t t0))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes
or
eq T (THead k t t0) (THead k t t0)
(eq T (THead k t t0) (THead k t t0))→∀P:Prop.P
by (refl_equal . .)
we proved eq T (THead k t t0) (THead k t t0)
by (or_introl . . previous)
or
eq T (THead k t t0) (THead k t t0)
(eq T (THead k t t0) (THead k t t0))→∀P:Prop.P
or
eq T (THead k t t0) (THead k0 t t0)
(eq T (THead k t t0) (THead k0 t t0))→∀P:Prop.P
case or_intror : H10:(eq K k k0)→∀P:Prop.P ⇒
the thesis becomes
or
eq T (THead k t t0) (THead k0 t t0)
(eq T (THead k t t0) (THead k0 t t0))→∀P:Prop.P
suppose H11: eq T (THead k t t0) (THead k0 t t0)
assume P: Prop
(H12)
by (f_equal . . . . . H11)
we proved
eq
K
<λ:T.K> CASE THead k t t0 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
<λ:T.K> CASE THead k0 t t0 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1 (THead k t t0)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1 (THead k0 t t0)
end of H12
(H13)
consider H12
we proved
eq
K
<λ:T.K> CASE THead k t t0 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
<λ:T.K> CASE THead k0 t t0 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
that is equivalent to eq K k k0
by (eq_ind_r . . . H10 . previous)
(eq K k k)→∀P0:Prop.P0
end of H13
by (refl_equal . .)
we proved eq K k k
by (H13 previous .)
we proved P
we proved (eq T (THead k t t0) (THead k0 t t0))→∀P:Prop.P
by (or_intror . . previous)
or
eq T (THead k t t0) (THead k0 t t0)
(eq T (THead k t t0) (THead k0 t t0))→∀P:Prop.P
or
eq T (THead k t t0) (THead k0 t t0)
(eq T (THead k t t0) (THead k0 t t0))→∀P:Prop.P
or
eq T (THead k t t0) (THead k0 t t4)
(eq T (THead k t t0) (THead k0 t t4))→∀P:Prop.P
case or_intror : H7:(eq T t0 t4)→∀P:Prop.P ⇒
the thesis becomes
or
eq T (THead k t t0) (THead k0 t t4)
(eq T (THead k t t0) (THead k0 t t4))→∀P:Prop.P
suppose H8: eq T (THead k t t0) (THead k0 t t4)
assume P: Prop
(H9)
by (f_equal . . . . . H8)
we proved
eq
K
<λ:T.K> CASE THead k t t0 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
<λ:T.K> CASE THead k0 t t4 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1 (THead k t t0)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1 (THead k0 t t4)
end of H9
(h1)
(H10)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:T.T> CASE THead k t t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t5⇒t5
<λ:T.T> CASE THead k0 t t4 OF TSort ⇒t0 | TLRef ⇒t0 | THead t5⇒t5
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t5⇒t5 (THead k t t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t5⇒t5 (THead k0 t t4)
end of H10
suppose : eq K k k0
(H12)
consider H10
we proved
eq
T
<λ:T.T> CASE THead k t t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t5⇒t5
<λ:T.T> CASE THead k0 t t4 OF TSort ⇒t0 | TLRef ⇒t0 | THead t5⇒t5
that is equivalent to eq T t0 t4
by (eq_ind_r . . . H7 . previous)
(eq T t0 t0)→∀P0:Prop.P0
end of H12
by (refl_equal . .)
we proved eq T t0 t0
by (H12 previous .)
we proved P
(eq K k k0)→P
end of h1
(h2)
consider H9
we proved
eq
K
<λ:T.K> CASE THead k t t0 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
<λ:T.K> CASE THead k0 t t4 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
eq K k k0
end of h2
by (h1 h2)
we proved P
we proved (eq T (THead k t t0) (THead k0 t t4))→∀P:Prop.P
by (or_intror . . previous)
or
eq T (THead k t t0) (THead k0 t t4)
(eq T (THead k t t0) (THead k0 t t4))→∀P:Prop.P
or
eq T (THead k t t0) (THead k0 t t4)
(eq T (THead k t t0) (THead k0 t t4))→∀P:Prop.P
or
eq T (THead k t t0) (THead k0 t3 t4)
(eq T (THead k t t0) (THead k0 t3 t4))→∀P:Prop.P
case or_intror : H4:(eq T t t3)→∀P:Prop.P ⇒
the thesis becomes
or
eq T (THead k t t0) (THead k0 t3 t4)
(eq T (THead k t t0) (THead k0 t3 t4))→∀P:Prop.P
suppose H5: eq T (THead k t t0) (THead k0 t3 t4)
assume P: Prop
(H6)
by (f_equal . . . . . H5)
we proved
eq
K
<λ:T.K> CASE THead k t t0 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
<λ:T.K> CASE THead k0 t3 t4 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1 (THead k t t0)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1 (THead k0 t3 t4)
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead k t t0 OF TSort ⇒t | TLRef ⇒t | THead t5 ⇒t5
<λ:T.T> CASE THead k0 t3 t4 OF TSort ⇒t | TLRef ⇒t | THead t5 ⇒t5
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t5 ⇒t5 (THead k t t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t5 ⇒t5 (THead k0 t3 t4)
end of H7
(h1)
(H8)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead k t t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t5⇒t5
<λ:T.T> CASE THead k0 t3 t4 OF TSort ⇒t0 | TLRef ⇒t0 | THead t5⇒t5
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t5⇒t5 (THead k t t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t5⇒t5 (THead k0 t3 t4)
end of H8
suppose H9: eq T t t3
suppose : eq K k k0
(H12)
by (eq_ind_r . . . H4 . H9)
(eq T t t)→∀P0:Prop.P0
end of H12
by (refl_equal . .)
we proved eq T t t
by (H12 previous .)
we proved P
(eq T t t3)→(eq K k k0)→P
end of h1
(h2)
consider H7
we proved
eq
T
<λ:T.T> CASE THead k t t0 OF TSort ⇒t | TLRef ⇒t | THead t5 ⇒t5
<λ:T.T> CASE THead k0 t3 t4 OF TSort ⇒t | TLRef ⇒t | THead t5 ⇒t5
eq T t t3
end of h2
by (h1 h2)
(eq K k k0)→P
end of h1
(h2)
consider H6
we proved
eq
K
<λ:T.K> CASE THead k t t0 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
<λ:T.K> CASE THead k0 t3 t4 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
eq K k k0
end of h2
by (h1 h2)
we proved P
we proved (eq T (THead k t t0) (THead k0 t3 t4))→∀P:Prop.P
by (or_intror . . previous)
or
eq T (THead k t t0) (THead k0 t3 t4)
(eq T (THead k t t0) (THead k0 t3 t4))→∀P:Prop.P
or
eq T (THead k t t0) (THead k0 t3 t4)
(eq T (THead k t t0) (THead k0 t3 t4))→∀P:Prop.P
we proved or (eq T (THead k t t0) t2) (eq T (THead k t t0) t2)→∀P:Prop.P
∀t2:T.(or (eq T (THead k t t0) t2) (eq T (THead k t t0) t2)→∀P:Prop.P)
we proved ∀t2:T.(or (eq T t1 t2) (eq T t1 t2)→∀P:Prop.P)
we proved ∀t1:T.∀t2:T.(or (eq T t1 t2) (eq T t1 t2)→∀P:Prop.P)