10 lines
148 B
Text
10 lines
148 B
Text
example (a b : Prop) (H : b ∧ a) : a ∧ b :=
|
|
begin
|
|
assert H : a
|
|
end
|
|
|
|
example (a : Prop) (Ha : a) : a :=
|
|
begin
|
|
exact Ha,
|
|
assert H : a
|
|
end
|