The Coq mailing list

[jean-francois.monin AT imag.fr]

Hi,

I did'nt read the complicated part, but at least:
> I would think if if I have a proof of type A /\ B, I must be able to
> show that the structure of that proof must be conj _ _; and hence, I
> should be able to simplify my and_rec, above. But I don't seem to be
> able to prove the following lemma:
> 
> Lemma and_conj : forall (A B:Prop) (pf : A /\ B), 
>   exists pa : A, exists pb : B, pf = conj pa pb.

intros. case pf. intros a b.
exists a. exists b.
reflexivity.
Qed.

Hope this helps,

-- 
Jean-François Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46