force lambda reduction

Stream: new members

[Michael Beeson]

I have this expression in a current proof:

h5: ∀ (x_1 : M), ¬¬(λ (k : M), k ∈ 𝔽 → x ∈ k → ¬¬x ∈ SSC U) x_1

and I want to force it to be lambda-reduced (without using classical logic) i.e., k will be replaced by x_1 and the lambda erased.

[Yury G. Kudryashov]

Try simp only.

[Yury G. Kudryashov]

with no lemmas

[Yury G. Kudryashov]

This is counter-intuitive but we have no dedicated tactic yet.

[Michael Beeson]

Thanks, that appeared to work. (Only when I finish the proof can I check if it really didn't use classical axioms, but it looks good.)

[Michael Beeson]

Is there a way to manually rename the bound variable x_1 (to something more pleasant to read)?

[Johan Commelin]

tactic#rename

[Yury G. Kudryashov]

replace h5 := λ x, h5 x?

[Mario Carneiro]

I usually use dsimp only to do "just beta reduction"