2014-10-28 23:08:39 +00:00
|
|
|
import logic
|
|
|
|
|
|
|
|
|
|
theorem test {A B : Type} {a : A} {b : B} (H : a == b) :
|
2016-01-09 20:32:18 +00:00
|
|
|
eq.rec_on (type_eq_of_heq H) a = b
|
2014-10-28 23:08:39 +00:00
|
|
|
:=
|
|
|
|
|
-- Remark the error message should not occur in the token theorem
|
|
|
|
|
heq.rec_on H rfl
|
