6 lines
69 B
Plaintext
6 lines
69 B
Plaintext
|
Goal A -> B -> C -> A.
|
||
|
|
intros.
|
||
|
|
apply.
|
||
|
|
exact.
|
||
|
|
assumption.
|
||
|
|
Qed.
|