7 lines
63 B
Plaintext
7 lines
63 B
Plaintext
(A /\ B) -> A
|
|
intro et.
|
|
elim et.
|
|
intro a.
|
|
intro b.
|
|
assumption.
|