Proof

Proof Summary of StrongNorm.thy:123

Isabelle Statement

source: StrongNorm.thy:123 benchmark: isa/deeper/B-mesh-th0/train2k problem: problems/HOL-Proofs-Lambda/0010_StrongNorm/prob_00123_003167.p

Lemma

lemma subst_type_IT:
  "⋀t e T u i. IT t ⟹ e⟨i:U⟩ ⊢ t : T ⟹
    IT u ⟹ e ⊢ u : U ⟹ IT (t[u/i])"
  (is "PROP ?P U" is "⋀t e T u i. _ ⟹ PROP ?Q t e T u i U")

Proof Excerpt

case (Cons a as)
with nT have "e⟨i:T⟩ ⊢ Var n ° a °° as : T'" by simp
then obtain Ts
    where headT: "e⟨i:T⟩ ⊢ Var n ° a : Ts ⇛ T'"
    and argsT: "e⟨i:T⟩ ⊩ as : Ts"
  by (rule list_app_typeE)

Conjectures

c_0_0

? [X1369: list_type] :
  ( ( typing @ ( shift_type @ e @ i @ t2 ) @ ( app @ ( var @ n ) @ a ) @ ( foldr_type_type @ fun @ X1369 @ t ) )
  & ( typings @ ( shift_type @ e @ i @ t2 ) @ as @ X1369 )
  & ~ thesis )

Axioms

c_0_2 c_0_3 c_0_4 c_0_5 c_0_6

Final Contradiction

c_0_37