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	instantiation	1, 2, 3	⊢
	: , : , :
1	reference	10	⊢
2	generalization	4	⊢
3	instantiation	5	⊢
	: , :
4	modus ponens	6, 7	⊢
5	axiom		⊢
	proveit.logic.sets.inclusion.subset_eq_def
6	instantiation	10, 8, 9	⊢
	: , : , :
7	assumption		⊢
8	instantiation	10, 11, 12	⊢
	: , : , :
9	instantiation	16, 13, 14	⊢
	: , : , :
10	theorem		⊢
	proveit.logic.equality.sub_left_side_into
11	deduction	15	⊢
12	instantiation	16, 32, 17	⊢
	: , : , :
13	theorem		⊢
	proveit.numbers.numerals.decimals.nat5
14	instantiation	18	⊢
	: , : , : , : , :
15	instantiation	21, 19, 20	⊢
	: , : , :
16	axiom		⊢
	proveit.logic.sets.enumeration.enum_set_def
17	instantiation	42	⊢
	: , : , :
18	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
19	instantiation	21, 22, 23	⊢
	: , : , :
20	instantiation	27, 32, 36, 39, 24, 41, 28, 50, 29, 30, 51	⊢
	: , : , : , : , : , : , :
21	theorem		⊢
	proveit.logic.equality.sub_right_side_into
22	instantiation	31, 32, 38, 39, 33, 25, 41, 26	⊢
	: , : , : , : , : , :
23	instantiation	27, 36, 38, 35, 28, 29, 30, 50, 51	⊢
	: , : , : , : , : , : , :
24	instantiation	42	⊢
	: , : , :
25	instantiation	46	⊢
	: , :
26	instantiation	31, 39, 32, 36, 41, 33, 34	⊢
	: , : , : , : , : , :
27	theorem		⊢
	proveit.logic.booleans.disjunction.leftward_commutation
28	instantiation	37, 39, 38, 41, 35, 44	⊢
	: , : , : , : , :
29	instantiation	37, 36, 44	⊢
	: , : , : , : , :
30	instantiation	37, 38, 39, 40, 41, 44	⊢
	: , : , : , : , :
31	theorem		⊢
	proveit.logic.booleans.disjunction.disassociate
32	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
33	instantiation	42	⊢
	: , : , :
34	instantiation	43, 44, 45, 48	⊢
	: , :
35	instantiation	46	⊢
	: , :
36	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
37	theorem		⊢
	proveit.logic.booleans.disjunction.each_is_bool
38	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
39	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
40	instantiation	46	⊢
	: , :
41	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
42	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
43	theorem		⊢
	proveit.logic.booleans.disjunction.or_if_left
44	instantiation	47, 48	⊢
	:
45	instantiation	49, 50, 51	⊢
	: , :
46	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
47	theorem		⊢
	proveit.logic.booleans.in_bool_if_true
48	assumption		⊢
49	theorem		⊢
	proveit.logic.booleans.disjunction.binary_closure
50	instantiation	52	⊢
	: , :
51	instantiation	52	⊢
	: , :
52	axiom		⊢
	proveit.logic.equality.equality_in_bool