2014-07-07 21:41:14 +00:00
|
|
|
|
import standard
|
2014-08-15 20:27:18 +00:00
|
|
|
|
using prod
|
2014-07-07 21:41:14 +00:00
|
|
|
|
|
|
|
|
|
|
inductive t1 : Type :=
|
|
|
|
|
|
| mk1 : t1
|
|
|
|
|
|
|
|
|
|
|
|
inductive t2 : Type :=
|
|
|
|
|
|
| mk2 : t2
|
|
|
|
|
|
|
|
|
|
|
|
theorem inhabited_t1 : inhabited t1
|
2014-08-20 22:49:44 +00:00
|
|
|
|
:= inhabited_mk mk1
|
2014-07-07 21:41:14 +00:00
|
|
|
|
|
|
|
|
|
|
theorem inhabited_t2 : inhabited t2
|
2014-08-20 22:49:44 +00:00
|
|
|
|
:= inhabited_mk mk2
|
2014-07-07 21:41:14 +00:00
|
|
|
|
|
|
|
|
|
|
instance inhabited_t1 inhabited_t2
|
|
|
|
|
|
|
|
|
|
|
|
theorem T : inhabited (t1 × t2)
|
|
|
|
|
|
:= _
|
|
|
|
|
|
|
