multiApp is wrong

[lengyijun]

theorem foo {f a b: Term String} : multiApp f (a :: b :: []) = (f.app b).app a := by
  grind

Should we change the documentation or the definition?

I found it when proving

theorem foo {f a: Term String} {l} : f.abs.LC -> a.LC -> multiApp f.abs (a :: l) ⭢ℓ  multiApp (f^a) l := by
  induction l generalizing f a with
  | nil => apply BetaAt.outer
  | cons head tail ih =>  intros _ _
                          unfold multiApp
                          sorry

@m-ow @chenson2018

[chenson2018]

I see, so the direction is reversed of what the doc indicate so that multiApp f [x₁, x₂, ..., xₙ] is (((f xₙ) xₙ₋₁) ... x₁)? If you need this to more easily state theorems like your example, you can change this definition to match the docs (though I think it'll be a bit of a pain). If it's not urgent for you, a PR just fixing the docs is also welcome.

[lengyijun]

I will try to fix the definition