The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Rob Dockins wrote:
> Is is possible to prove the following two lemmas?  It seems to me like they 
> should be true, but I can't figure out a way to tackle the proof.
>
> Lemma unit_not_pair : forall A B:Type, prodT A B <> unit.
> Lemma pair_eq_inj : forall A A' B B',
>     prodT A B = prodT A' B' -> A = A' /\ B = B'.
>   

I wouldn't be surprised if both lemmas are independent of 
CIC-sans-axioms.  I certainly don't know how to prove either.

However, if you specialize the first lemma such that at least one of [A] 
and [B] has at least two distinct members, then you get a fairly 
straightforward proof by a cardinality argument.  I've done many such 
proofs for theorems like [Empty_set <> unit], which tend to pop up in 
denotational approaches to language semantics.