blob: 27a9ebe15d1a4849b08dc926bcacc1833482d2da (
plain)
1
2
3
4
5
6
7
8
|
Inductive Cube:Set :=| Triple: nat -> nat -> nat -> Cube.
Theorem incomplete :forall a b c d : nat,Triple a = Triple b->Triple d c = Triple d b->a = c.
Proof.
Fail congruence.
intros.
congruence with ((Triple a a a)) ((Triple d c a)).
Qed.
|
