no goals
as ps : List Prop
p : Prop
as₁ : List Prop
⊢ as = List.reverseAux as₁ ps → implies (mk as) p ps (List.length as₁) → p
induction ps generalizing as₁ with
| nil => exact fun _ ↦ id
| cons a as ih =>
  refine fun e H ↦ @ih (a::as₁) e (H ?_)
  subst e; clear ih H
  suffices ∀ n n', n' = List.length as₁ + n →
    ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a::as)
  induction as₁ with simp
  | cons b as₁ ih => exact fun n bs ↦ ih (n+1) _ (Nat.succ_add ..) _
no goals
case nil
as : List Prop
p : Prop
as₁ : List Prop
⊢ as = List.reverseAux as₁ [] → implies (mk as) p [] (List.length as₁) → p
exact fun _ ↦ id
case cons
as✝ : List Prop
p a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = List.reverseAux as₁ as → implies (mk as✝) p as (List.length as₁) → p
as₁ : List Prop
e : as✝ = List.reverseAux as₁ (a :: as)
H : implies (mk as✝) p (a :: as) (List.length as₁)
⊢ mk as✝ (List.length as₁) ↔ a
case cons
as✝ : List Prop
p a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = List.reverseAux as₁ as → implies (mk as✝) p as (List.length as₁) → p
as₁ : List Prop
⊢ as✝ = List.reverseAux as₁ (a :: as) → implies (mk as✝) p (a :: as) (List.length as₁) → p
refine fun e H ↦ @ih (a::as₁) e (H ?_)
case cons
p a : Prop
as as₁ : List Prop
ih :
  ∀ (as₁_1 : List Prop),
    List.reverseAux as₁ (a :: as) = List.reverseAux as₁_1 as →
      implies (mk (List.reverseAux as₁ (a :: as))) p as (List.length as₁_1) → p
H : implies (mk (List.reverseAux as₁ (a :: as))) p (a :: as) (List.length as₁)
⊢ mk (List.reverseAux as₁ (a :: as)) (List.length as₁) ↔ a
case cons
as✝ : List Prop
p a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = List.reverseAux as₁ as → implies (mk as✝) p as (List.length as₁) → p
as₁ : List Prop
e : as✝ = List.reverseAux as₁ (a :: as)
H : implies (mk as✝) p (a :: as) (List.length as₁)
⊢ mk as✝ (List.length as₁) ↔ a
subst e
case cons
p a : Prop
as as₁ : List Prop
⊢ mk (List.reverseAux as₁ (a :: as)) (List.length as₁) ↔ a
case cons
p a : Prop
as as₁ : List Prop
ih :
  ∀ (as₁_1 : List Prop),
    List.reverseAux as₁ (a :: as) = List.reverseAux as₁_1 as →
      implies (mk (List.reverseAux as₁ (a :: as))) p as (List.length as₁_1) → p
H : implies (mk (List.reverseAux as₁ (a :: as))) p (a :: as) (List.length as₁)
⊢ mk (List.reverseAux as₁ (a :: as)) (List.length as₁) ↔ a
clear ih H
case cons
p a : Prop
as as₁ : List Prop
⊢ ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
case cons
p a : Prop
as as₁ : List Prop
⊢ mk (List.reverseAux as₁ (a :: as)) (List.length as₁) ↔ a
suffices ∀ n n', n' = List.length as₁ + n →
  ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a::as)
no goals
case cons
p a : Prop
as as₁ : List Prop
⊢ ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
induction as₁ with simp
| cons b as₁ ih => exact fun n bs ↦ ih (n+1) _ (Nat.succ_add ..) _
no goals
case cons.cons
p a : Prop
as : List Prop
b : Prop
as₁ : List Prop
ih : ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
⊢ ∀ (n : ℕ) (bs : List Prop), mk (List.reverseAux as₁ (b :: bs)) (Nat.succ (List.length as₁) + n) ↔ mk bs n
exact fun n bs ↦ ih (n+1) _ (Nat.succ_add ..) _