Theorem: ListN.append_nil (GMLInit/Data/List/ListN.lean)

State before:
α : Type u_1
n : Nat
xs : ListN α n
⊢ xs.append nil ≅ xs
Tactic:
cases xs
State after:
case mk
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ { toList := toList✝, length_eq := length_eq✝ }.append nil ≅ { toList := toList✝, length_eq := length_eq✝ }

State before:
case mk
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ { toList := toList✝, length_eq := length_eq✝ }.append nil ≅ { toList := toList✝, length_eq := length_eq✝ }
Tactic:
apply ListN.heq
State after:
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ α = α

case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ 0 + n = n

case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ ({ toList := toList✝, length_eq := length_eq✝ }.append nil).toList ≅
    { toList := toList✝, length_eq := length_eq✝ }.toList

State before:
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ α = α
Tactic:
rfl
State after:
no goals

State before:
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ 0 + n = n
Tactic:
rw [Nat.zero_add]
State after:
no goals

State before:
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ ({ toList := toList✝, length_eq := length_eq✝ }.append nil).toList ≅
    { toList := toList✝, length_eq := length_eq✝ }.toList
Tactic:
simp only [ListN.append]
State after:
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ toList✝ ++ [] ≅ toList✝

State before:
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ toList✝ ++ [] ≅ toList✝
Tactic:
rw [List.append_nil]
State after:
no goals