The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

I believe intros. trivial. should do Theo job.

Em seg, 14 de mai de 2018 07:03, Gergely Buday <gbuday AT gmail.com> escreveu:

Hi,

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros  b c. destruct c.
  - reflexivity.
  - destruct b.
    + simpl.

leads to

1 subgoal
______________________________________(1/1)
false = true -> false = true

which is clearly true but I do not see how this can be resolved with
the tools mentioned in Software Foundations.

I would think of both the premise and the conclusion evaluates to the
builtin_false constant because of the nature of inductive definitions

and then by the usual truth table line

  builtin_false -> builtin_false

should be true.

How can I make this work in Coq?

- Gergely