8 lines
111 B
Text
8 lines
111 B
Text
|
import logic
|
||
|
|
|
||
|
|
example (a b c : Prop) (h : a) : true → true → a :=
|
||
|
|
begin
|
||
|
|
rewrite *true_imp,
|
||
|
|
exact h
|
||
|
|
end
|