no goals
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
head✝ : α
tail✝ : List α
h1 : length (head✝ :: tail✝) = length []
x✝ : Equiv (head✝ :: tail✝) []
⊢ head✝ :: tail✝ = []
cases h1
no goals
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
head✝ : α
tail✝ : List α
h1 : length [] = length (head✝ :: tail✝)
x✝ : Equiv [] (head✝ :: tail✝)
⊢ [] = head✝ :: tail✝
cases h1
case e_head
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
⊢ a1 = a2

case e_tail
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
⊢ as1 = as2
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
⊢ a1 :: as1 = a2 :: as2
congr
no goals
case e_head
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
⊢ a1 = a2
apply h2 0
case e_tail
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
h3 : length as1 = length as2
⊢ as1 = as2
case e_tail
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
⊢ as1 = as2
have h3 : as1.length = as2.length := by simpa [add_left_inj, add_comm, length] using h1
case e_tail
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
h3 : length as1 = length as2
⊢ Equiv as1 as2
case e_tail
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
h3 : length as1 = length as2
⊢ as1 = as2
apply eq_of_equiv h3
case e_tail
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
h3 : length as1 = length as2
m : ℕ
⊢ get m as1 = get m as2
case e_tail
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
h3 : length as1 = length as2
⊢ Equiv as1 as2
intro m
no goals
case e_tail
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
h3 : length as1 = length as2
m : ℕ
⊢ get m as1 = get m as2
apply h2 (m + 1)
no goals
α : Type u
β : Type v
γ : Type w
a : α
as as1✝ as2✝ as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
a1 : α
as1 : List α
a2 : α
as2 : List α
h1 : length (a1 :: as1) = length (a2 :: as2)
h2 : Equiv (a1 :: as1) (a2 :: as2)
⊢ length as1 = length as2
simpa [add_left_inj, add_comm, length] using h1