30 lines
405 B
Text
30 lines
405 B
Text
variable P : Prop
|
|
premise HP : P
|
|
|
|
example : P :=
|
|
have H : P, from HP,
|
|
H
|
|
|
|
example : P :=
|
|
have H : P, from HP,
|
|
show P, from H
|
|
|
|
example : P :=
|
|
have H : P, from HP,
|
|
by exact H
|
|
|
|
example : P :=
|
|
have H : P, from HP,
|
|
show P, by exact H
|
|
|
|
example : P :=
|
|
have H : P, from HP,
|
|
show P, begin exact H end
|
|
|
|
example : P :=
|
|
have H : P, from HP,
|
|
show P, by exact H
|
|
|
|
example : P :=
|
|
assert H : P, from HP,
|
|
show P, by exact H
|