## Stream: Beginner Questions

### Topic: ✔ Failure to apply induction on a theorem

#### Mathias Fleury (Sep 04 2022 at 15:30):

Simpler version: always use `==>`

#### Mathias Fleury (Sep 04 2022 at 15:30):

Only exception: when you work under \forall

#### Notification Bot (Sep 04 2022 at 16:02):

Alex Weisberger has marked this topic as resolved.

#### Wolfgang Jeltsch (Sep 04 2022 at 17:12):

Mathias Fleury said:

Only exception: when you work under \forall

But then, when do you work under ∀? You can and usually should use ⋀ instead. You have to use ⟶ and ∀ only where you have to use `bool`, which typically is in a definition.

#### Alex Weisberger (Sep 05 2022 at 00:50):

``````theorem "⟦beval1 t t'; beval1 t t''⟧ ⟹ t' = t''"
``````

This seems to work as well, and for me is a little more clear because the premises are clearly grouped together.

#### Mathias Fleury (Sep 05 2022 at 04:24):

Wolfgang Jeltsch said:
You have to use ⟶ and ∀ only where you have to use `bool`, which typically is in a definition.

This is what i meant with \forall…

Wolfgang Jeltsch said:
But then, when do you work under ∀? You can and usually should use ⋀ instead.

I don't agree: all tactics and compositon work on `==>` and `!!` (induction, rule, OF, of, ...). Hence the default choice for theorems should always be the Pure symbols

#### Wolfgang Jeltsch (Sep 05 2022 at 11:09):

Mathias Fleury said:

Wolfgang Jeltsch said:
But then, when do you work under ∀? You can and usually should use ⋀ instead.

I don't agree: all tactics and compositon work on `==>` and `!!` (induction, rule, OF, of, ...). Hence the default choice for theorems should always be the Pure symbols

Isn’t this what I said above? :wink:

#### Mathias Fleury (Sep 05 2022 at 11:10):

ah sorry I misunderstood you then…

#### Mathias Fleury (Sep 05 2022 at 11:10):

I thought that your `You can and usually should use ⋀ instead` was meant in general, and not only below ∀

#### Wolfgang Jeltsch (Sep 05 2022 at 17:09):

Mathias Fleury said:

I thought that your `You can and usually should use ⋀ instead` was meant in general, and not only below ∀

Of course, it was meant in general, and that’s what you’re saying as well, right? I mean, `⋀` is the same as `!!`, a pure symbol, and you’re saying, “Hence the default choice for theorems should always be the Pure symbols”.

#### Mathias Fleury (Sep 05 2022 at 18:03):

I find ‹⋀∧› and `⋀∧` too hard to distinguish

Last updated: Feb 27 2024 at 08:17 UTC