The Coq mailing list

["Theodoros G. Tsokos" <T.Tsokos AT cs.bham.ac.uk>]

> >
> Well, for lack of more information, I assume that op_and is also a 
> constructor of the term type.
> Starting from your goal:
>
> H1 : FF G b1 -> FF G v1
> H2 : ...
> =====
> FF G (op_and b1 b2) -> FF G (v1 && v2)
>
> I would simply use inversion, in the following way:
>
> intros HA; inversion HA.
>
> This would yield two hypotheses with statements:
>
> FF G b1
>
> and
>
> FF G b2
>
> and then it would be possible to conclude, by case analysis on v1 
> (tactic destruct), and
> a second case analysis on v2 in the case where v1 is true.
>
> Tell me if this helps.
>
> Yves
Yes, it helps a lot, thanks a lot!

Yes, op_and is a constructor of the term type as well. The proof is 
almost done now, apart from the function term. But the important thing 
was to advance the proof, so thanks indeed.

Regards,
Theo.

--
| Theodoros G. Tsokos                                      |
| http://www.cs.bham.ac.uk/~txt                            ;|
| School of Computer Science, The University of Birmingham |
| Edgbaston, Birmingham, B15 2TT, United Kingdom           |
| -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- |
| "The freedom of speech includes the freedom to shut up"  |
| -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- |
| "Democracy: the freedom to say whatever one wants and    |
| the capital to implement whatever it wants"              |
--