IH1 : false = true -> false = true

goal: false = true

Above IH1 may helpful in solving goal statement?

No, it is not possible to prove the given goal from the assumption.

You cannot prove something which is contradictory (false = true) unless your assumptions are themselves contradictory.

However, it is not a contradiction that (false = true -> false = true). This is perfectly sound, it is a tautology of propositional logic

when we have false=true in hypothesis, then we can prove any thing from it. Then why i am unable to prove false=true here?

Is there any difference between false=true & false=true->false=true?

Your sentence "we have false=true in hypothesis" is quite ambiguous. The contradiction holds when your hypothesis *is* just `false=true`

. But, as Patrick mentionned, a proposition which may *contain* `false=true`

, like `false=true -> false= true`

, may be non-contradictory.

```
Goal false = true -> 2 = 3.
intro; discriminate.
Qed.
Goal (false = true -> false = true) -> 2= 3.
intro H; discriminate H. (* stuck *)
Abort.
```

Last updated: Jun 20 2024 at 13:02 UTC