no goals
motive : List Nat → Sort u
l : List Nat
empty : motive []
single : (a : Nat) → motive [a]
step : (a b : Nat) → (l : List Nat) → motive (b :: l) → motive (a :: b :: l)
⊢ motive l
induction l with
| nil => assumption
| cons a l => cases l; apply single; apply step; assumption
no goals
case nil
motive : List Nat → Sort u
empty : motive []
single : (a : Nat) → motive [a]
step : (a b : Nat) → (l : List Nat) → motive (b :: l) → motive (a :: b :: l)
⊢ motive []
assumption
case cons.nil
motive : List Nat → Sort u
empty : motive []
single : (a : Nat) → motive [a]
step : (a b : Nat) → (l : List Nat) → motive (b :: l) → motive (a :: b :: l)
a : Nat
tail_ih✝ : motive []
⊢ motive [a]

case cons.cons
motive : List Nat → Sort u
empty : motive []
single : (a : Nat) → motive [a]
step : (a b : Nat) → (l : List Nat) → motive (b :: l) → motive (a :: b :: l)
a head✝ : Nat
tail✝ : List Nat
tail_ih✝ : motive (head✝ :: tail✝)
⊢ motive (a :: head✝ :: tail✝)
case cons
motive : List Nat → Sort u
empty : motive []
single : (a : Nat) → motive [a]
step : (a b : Nat) → (l : List Nat) → motive (b :: l) → motive (a :: b :: l)
a : Nat
l : List Nat
tail_ih✝ : motive l
⊢ motive (a :: l)
cases l
case cons.cons
motive : List Nat → Sort u
empty : motive []
single : (a : Nat) → motive [a]
step : (a b : Nat) → (l : List Nat) → motive (b :: l) → motive (a :: b :: l)
a head✝ : Nat
tail✝ : List Nat
tail_ih✝ : motive (head✝ :: tail✝)
⊢ motive (a :: head✝ :: tail✝)
case cons.nil
motive : List Nat → Sort u
empty : motive []
single : (a : Nat) → motive [a]
step : (a b : Nat) → (l : List Nat) → motive (b :: l) → motive (a :: b :: l)
a : Nat
tail_ih✝ : motive []
⊢ motive [a]

case cons.cons
motive : List Nat → Sort u
empty : motive []
single : (a : Nat) → motive [a]
step : (a b : Nat) → (l : List Nat) → motive (b :: l) → motive (a :: b :: l)
a head✝ : Nat
tail✝ : List Nat
tail_ih✝ : motive (head✝ :: tail✝)
⊢ motive (a :: head✝ :: tail✝)
apply single
case cons.cons.a
motive : List Nat → Sort u
empty : motive []
single : (a : Nat) → motive [a]
step : (a b : Nat) → (l : List Nat) → motive (b :: l) → motive (a :: b :: l)
a head✝ : Nat
tail✝ : List Nat
tail_ih✝ : motive (head✝ :: tail✝)
⊢ motive (head✝ :: tail✝)
case cons.cons
motive : List Nat → Sort u
empty : motive []
single : (a : Nat) → motive [a]
step : (a b : Nat) → (l : List Nat) → motive (b :: l) → motive (a :: b :: l)
a head✝ : Nat
tail✝ : List Nat
tail_ih✝ : motive (head✝ :: tail✝)
⊢ motive (a :: head✝ :: tail✝)
apply step
no goals
case cons.cons.a
motive : List Nat → Sort u
empty : motive []
single : (a : Nat) → motive [a]
step : (a b : Nat) → (l : List Nat) → motive (b :: l) → motive (a :: b :: l)
a head✝ : Nat
tail✝ : List Nat
tail_ih✝ : motive (head✝ :: tail✝)
⊢ motive (head✝ :: tail✝)
assumption