feat: decidable LcAt and LC

[lengyijun]

This PR makes LcAt and LC decidable.

Before:

def Term_LA0L1 : Term String := .abs (.app (.bvar 0) (.abs (.bvar 1)))

theorem LA0L1_lc : Term_LA0L1.LC := by
unfold Term_LA0L1
apply LC.abs
intros
simp [open', openRec]
apply LC.app
grind
apply LC.abs
intros
simp [open', openRec]
grind
exact ∅
exact ∅

After:

theorem LA0L1_lc : LcAt 0 Term_LA0L1 := by decide

[lengyijun]

I don't understand what's problem of pr title

[chenson2018]

I don't understand what's problem of pr title

It had some leading whitespace.

[chenson2018]

If making LcAt decidable, we should also use lcAt_iff_LC (later in this file) to also get a Decidable instance for LC.

[chenson2018]

(see my above comments)

[chenson2018]

I see you requested my review again, but I don't see a new commit. In case I was unclear, what I intended was for you to add something like

instance [HasFresh Var] [DecidableEq Var] (t : Term Var) : Decidable t.LC := by
  rw [← lcAt_iff_LC]
  infer_instance

in this file.

[lengyijun]

@chenson2018 DecidableEq Var looks unnecessary ?

[chenson2018]

@chenson2018 DecidableEq Var looks unnecessary ?

You're right, thanks for catching that!

[chenson2018]

Looks good, thanks!