Show the Proof

import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof

	step type	requirements	statement
0	deduction	1	,  ⊢
1	instantiation	17, 2, 3	, ,  ⊢
	:
2	generalization	4	,  ⊢
3	modus ponens	5, 6	,  ⊢
4	instantiation	7, 8	, ,  ⊢
	: , :
5	instantiation	9, 10	⊢
	:
6	instantiation	11, 27	⊢
	: , :
7	theorem		⊢
	proveit.logic.equality.fold_not_equals
8	instantiation	12, 13, 14	, ,  ⊢
	:
9	theorem		⊢
	proveit.logic.booleans.quantification.existence.exists_unfolding
10	assumption		⊢
11	theorem		⊢
	proveit.logic.booleans.conjunction.left_from_and
12	axiom		⊢
	proveit.logic.booleans.implication.denial_via_contradiction
13	instantiation	15	⊢
	: , :
14	deduction	16	, ,  ⊢
15	axiom		⊢
	proveit.logic.equality.equality_in_bool
16	instantiation	17, 18, 19	, , ,  ⊢
	:
17	theorem		⊢
	proveit.logic.booleans.negation.negation_contradiction
18	modus ponens	20, 21	, ,  ⊢
19	assumption		⊢
20	instantiation	22, 23	,  ⊢
	:
21	instantiation	24, 25	⊢
	:
22	instantiation	26, 27	⊢
	: , :
23	assumption		⊢
24	axiom		⊢
	proveit.logic.booleans.eq_true_elim
25	assumption		⊢
26	theorem		⊢
	proveit.logic.booleans.conjunction.right_from_and
27	assumption		⊢