DEFINITION csubst0_gen_sort()
TYPE =
∀x:C.∀v:T.∀i:nat.∀n:nat.(csubst0 i v (CSort n) x)→∀P:Prop.P
BODY =
assume x: C
assume v: T
assume i: nat
assume n: nat
suppose H: csubst0 i v (CSort n) x
assume P: Prop
assume y: C
suppose H0: csubst0 i v y x
we proceed by induction on H0 to prove (eq C y (CSort n))→P
case csubst0_snd : k:K i0:nat v0:T u1:T u2:T :subst0 i0 v0 u1 u2 c:C ⇒
the thesis becomes ∀H2:(eq C (CHead c k u1) (CSort n)).P
suppose H2: eq C (CHead c k u1) (CSort n)
(H3)
we proceed by induction on H2 to prove <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
case refl_equal : ⇒
the thesis becomes <λ:C.Prop> CASE CHead c k u1 OF CSort ⇒False | CHead ⇒True
consider I
we proved True
<λ:C.Prop> CASE CHead c k u1 OF CSort ⇒False | CHead ⇒True
<λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
end of H3
consider H3
we proved <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
∀H2:(eq C (CHead c k u1) (CSort n)).P
case csubst0_fst : k:K i0:nat c1:C c2:C v0:T :csubst0 i0 v0 c1 c2 u:T ⇒
the thesis becomes ∀H3:(eq C (CHead c1 k u) (CSort n)).P
() by induction hypothesis we know (eq C c1 (CSort n))→P
suppose H3: eq C (CHead c1 k u) (CSort n)
(H4)
we proceed by induction on H3 to prove <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
case refl_equal : ⇒
the thesis becomes <λ:C.Prop> CASE CHead c1 k u OF CSort ⇒False | CHead ⇒True
consider I
we proved True
<λ:C.Prop> CASE CHead c1 k u OF CSort ⇒False | CHead ⇒True
<λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
end of H4
consider H4
we proved <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
∀H3:(eq C (CHead c1 k u) (CSort n)).P
case csubst0_both : k:K i0:nat v0:T u1:T u2:T :subst0 i0 v0 u1 u2 c1:C c2:C :csubst0 i0 v0 c1 c2 ⇒
the thesis becomes ∀H4:(eq C (CHead c1 k u1) (CSort n)).P
() by induction hypothesis we know (eq C c1 (CSort n))→P
suppose H4: eq C (CHead c1 k u1) (CSort n)
(H5)
we proceed by induction on H4 to prove <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
case refl_equal : ⇒
the thesis becomes <λ:C.Prop> CASE CHead c1 k u1 OF CSort ⇒False | CHead ⇒True
consider I
we proved True
<λ:C.Prop> CASE CHead c1 k u1 OF CSort ⇒False | CHead ⇒True
<λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
end of H5
consider H5
we proved <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
∀H4:(eq C (CHead c1 k u1) (CSort n)).P
we proved (eq C y (CSort n))→P
we proved ∀y:C.(csubst0 i v y x)→(eq C y (CSort n))→P
by (insert_eq . . . . previous H)
we proved P
we proved ∀x:C.∀v:T.∀i:nat.∀n:nat.(csubst0 i v (CSort n) x)→∀P:Prop.P