α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive (size as) init
f : α → β → β
hf : ∀ (i : Fin (size as)) (b : β), motive (i.val + 1) b → motive i.val (f as[i] b)
this :
  (∀ (i : Fin (size as)) (b : β), motive (i.val + 1) b → SatisfiesM (motive i.val) (f as[i] b)) →
    SatisfiesM (motive 0) (foldrM f init as (size as))
⊢ motive 0 (foldr f init as (size as))
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive (size as) init
f : α → β → β
hf : ∀ (i : Fin (size as)) (b : β), motive (i.val + 1) b → motive i.val (f as[i] b)
⊢ motive 0 (foldr f init as (size as))
have := SatisfiesM_foldrM (m := Id) (as := as) (f := f) motive h0
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive (size as) init
f : α → β → β
hf : ∀ (i : Fin (size as)) (b : β), motive (i.val + 1) b → motive i.val (f as[i] b)
this :
  (∀ (i : Fin (size as)) (b : β), motive (i.val + 1) b → motive i.val (f as[i.val] b)) →
    motive 0 (foldrM f init as (size as))
⊢ motive 0 (foldr f init as (size as))
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive (size as) init
f : α → β → β
hf : ∀ (i : Fin (size as)) (b : β), motive (i.val + 1) b → motive i.val (f as[i] b)
this :
  (∀ (i : Fin (size as)) (b : β), motive (i.val + 1) b → SatisfiesM (motive i.val) (f as[i] b)) →
    SatisfiesM (motive 0) (foldrM f init as (size as))
⊢ motive 0 (foldr f init as (size as))
simp [SatisfiesM_Id_eq] at this
no goals
α : Type u_1
β : Type u_2
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive (size as) init
f : α → β → β
hf : ∀ (i : Fin (size as)) (b : β), motive (i.val + 1) b → motive i.val (f as[i] b)
this :
  (∀ (i : Fin (size as)) (b : β), motive (i.val + 1) b → motive i.val (f as[i.val] b)) →
    motive 0 (foldrM f init as (size as))
⊢ motive 0 (foldr f init as (size as))
exact this hf