11 lines
142 B
Text
11 lines
142 B
Text
import logic
|
|
|
|
definition id {A : Type} (a : A) := a
|
|
|
|
theorem tst (a : Prop) : a → id a :=
|
|
begin
|
|
intro Ha,
|
|
whnf,
|
|
state,
|
|
apply Ha
|
|
end
|