α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ Lists' α b
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ Lists' α true
rw [h]
no goals
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ Lists' α b
exact l
no goals
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α b) l;
  ofList (toList l') = l'
induction l with
| atom => cases h
| nil => simp
| cons' b a _ IH =>
  intro l'
  simpa [cons] using IH rfl
no goals
case atom
α : Type u_1
b : Bool
a✝ : α
h : true = false
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α false) (atom a✝);
  ofList (toList l') = l'
cases h
no goals
case nil
α : Type u_1
b : Bool
h : true = true
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α true) nil;
  ofList (toList l') = l'
simp
case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α b✝) b;
    ofList (toList l') = l'
IH :
  ∀ (h : true = true),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α true) a;
    ofList (toList l') = l'
h : true = true
l' : Lists' α true := Eq.mpr (_ : Lists' α true = Lists' α true) (cons' b a)
⊢ ofList (toList l') = l'
case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α b✝) b;
    ofList (toList l') = l'
IH :
  ∀ (h : true = true),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α true) a;
    ofList (toList l') = l'
h : true = true
⊢ let l' := Eq.mpr (_ : Lists' α true = Lists' α true) (cons' b a);
  ofList (toList l') = l'
intro l'
no goals
case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α b✝) b;
    ofList (toList l') = l'
IH :
  ∀ (h : true = true),
    let l' := Eq.mpr (_ : Lists' α true = Lists' α true) a;
    ofList (toList l') = l'
h : true = true
l' : Lists' α true := Eq.mpr (_ : Lists' α true = Lists' α true) (cons' b a)
⊢ ofList (toList l') = l'
simpa [cons] using IH rfl